I need to be able to use a variables that is a sequence of logic variables
Exactly, a general solution to this problem is to introduce an arbitrary, dynamic number of logic variables and relate/constrain them.
Solver
First define some recursive goals to work with sequences of logic variables. (Luckily I already had these around for previous problems!)
Relate the sum of a sequence of logic variables to another logic variable:
(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)])))
Relate the sum of products of two sequence of logic variables to another logic variable:
(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)])))
Plus a little helper function to generate the magnitude multipliers:
(defn magnitudes [n]
(reverse (take n (iterate #(* 10 %) 1))))
Then wire it all together:
(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))))
Some of this should look familiar from your example, but the major differences are that the number of words (and their characters) can be handled dynamically. Fresh logic variables are created with lvar for the set of all characters, as well as the sums for each word. Then the logic variables are constrained/related using everyg and the recursive goals above.
Sample Problems
The function will return all solutions for the given words, and "send more money" only has one possible solution:
(cryptarithmetic "send" "more" "money")
=> ({\s 9, \e 5, \n 6, \d 7, \m 1, \o 0, \r 8, \y 2})
Another example with four words is "cp is fun true" (see Google Cryptarithmetic Puzzles) which has 72 possible solutions:
(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}
...
This is the biggest one I could find is on Wikipedia, and the function finds the only solution in ~30s on my laptop:
(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})
And here's a function to pretty print the results:
(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
