Мне нужно иметь возможность использовать переменные, которые представляют собой последовательность логических переменных
Точно, общее решение этой проблемы - ввести произвольное, динамическое число логических переменных и их связывание / ограничение.
Solver
Сначала определите некоторые рекурсивные цели для работы с последовательностями логических переменных.(К счастью, у меня уже было это для предыдущих задач !)
Соотнесите сумму последовательности логических переменных с другой логической переменной:
(defn sumo [vars sum]
(fresh [vhead vtail run-sum]
(conde
[(== vars ()) (== sum 0)]
[(conso vhead vtail vars)
(fd/+ vhead run-sum sum)
(sumo vtail run-sum)])))
Соотнесите сумму произведений двух последовательностей логических переменных с другой логической переменной:
(defn productsumo [vars dens sum]
(fresh [vhead vtail dhead dtail product run-sum]
(conde
[(emptyo vars) (== sum 0)]
[(conso vhead vtail vars)
(conso dhead dtail dens)
(fd/* vhead dhead product)
(fd/+ product run-sum sum)
(productsumo vtail dtail run-sum)])))
Плюс небольшая вспомогательная функция для генерации множителей величины:
(defn magnitudes [n]
(reverse (take n (iterate #(* 10 %) 1))))
Затем соедините все это вместе:
(defn cryptarithmetic [& words]
(let [distinct-chars (distinct (apply concat words))
char->lvar (zipmap distinct-chars (repeatedly (count distinct-chars) lvar))
lvars (vals char->lvar)
first-letter-lvars (distinct (map #(char->lvar (first %)) words))
sum-lvars (repeatedly (count words) lvar)
word-lvars (map #(map char->lvar %) words)]
(run* [q]
(everyg #(fd/in % (fd/interval 0 9)) lvars) ;; digits 0-9
(everyg #(fd/!= % 0) first-letter-lvars) ;; no leading zeroes
(fd/distinct lvars) ;; only distinct digits
(everyg (fn [[sum l]] ;; calculate sums for each word
(productsumo l (magnitudes (count l)) sum))
(map vector sum-lvars word-lvars))
(fresh [s]
(sumo (butlast sum-lvars) s) ;; sum all input word sums
(fd/== s (last sum-lvars))) ;; input word sums must equal last word sum
(== q char->lvar))))
Некоторое из этого может показаться знакомым из вашего примера, но основные различия заключаются в том, что количество слов (и их символов)может быть обработан динамически.Свежие логические переменные создаются с lvar для набора всех символов, а также сумм для каждого слова.Затем логические переменные связываются / связываются с использованием everyg и рекурсивных целей, указанных выше.
Примеры задач
Функция вернет все решения для заданных слов и только "отправит больше денег"есть одно возможное решение:
(cryptarithmetic "send" "more" "money")
=> ({\s 9, \e 5, \n 6, \d 7, \m 1, \o 0, \r 8, \y 2})
Другой пример с четырьмя словами: «cp is fun true» (см. Google Cryptarithmetic Puzzles ), который имеет 72 возможных решения:
(cryptarithmetic "cp" "is" "fun" "true")
=>
({\c 2, \e 4, \f 9, \i 7, \n 3, \p 5, \r 0, \s 6, \t 1, \u 8}
{\c 2, \e 5, \f 9, \i 7, \n 3, \p 4, \r 0, \s 8, \t 1, \u 6}
{\c 2, \e 6, \f 9, \i 7, \n 3, \p 5, \r 0, \s 8, \t 1, \u 4}
...
Это самое большое, что я могу найти в Википедии , и функция находит единственное решение в ~ 30 с на моем ноутбуке:
(cryptarithmetic "SO" "MANY" "MORE" "MEN" "SEEM" "TO"
"SAY" "THAT" "THEY" "MAY" "SOON" "TRY"
"TO" "STAY" "AT" "HOME" "SO" "AS" "TO"
"SEE" "OR" "HEAR" "THE" "SAME" "ONE"
"MAN" "TRY" "TO" "MEET" "THE" "TEAM"
"ON" "THE" "MOON" "AS" "HE" "HAS"
"AT" "THE" "OTHER" "TEN" "TESTS")
=> ({\A 7, \E 0, \H 5, \M 2, \N 6, \O 1, \R 8, \S 3, \T 9, \Y 4})
А вот функция довольнораспечатать результаты:
(defn pprint-answer [char->digit words]
(let [nums (map #(apply str (map char->digit %))
words)
width (apply max (map count nums))
width-format (str "%" width "s")
pad #(format width-format %)]
(println
(clojure.string/join \newline
(concat
(map #(str "+ " (pad %)) (butlast nums))
[(apply str (repeat (+ 2 width) \-))
(str "= " (pad (last nums)))]))
\newline)))
(cryptarithmetic "wrong" "wrong" "right")
(map #(pprint-answer % ["wrong" "wrong" "right"]) *1)
; + 12734
; + 12734
; -------
; = 25468