Using apply in core.logic Clojure (CLP) Cryptoarithmetic

Question

(ns verbal-arithmetic
  (:require
    [clojure.core.logic :refer [all run* everyg lvar == membero fresh conde succeed fail conso resto]]
    [clojure.core.logic.fd :as fd]))

(comment
  "Solving cryptarithmetic puzzle"
  " SEND
  + MORE
  ______
   MONEY")


(defn send-more-money-solutions []
  (run* [s e n d m o r y]
        (fd/in s e n d m o r y (fd/interval 0 9))
        (fd/!= s 0)
        (fd/!= m 0)
        (fd/distinct [s e n d m o r y])
        (fd/eq (= (apply + [(* 1000 s) (* 100 e) (* 10 n) d
                            (* 1000 m) (* 100 o) (* 10 r) e])
                  (apply + [(* 10000 m) (* 1000 o) (* 100 n) (* 10 e) y])))))

The above example doesn't work because apply does not work correctly in fd/eq. The following version of send-more-money-solutions works because I don't use apply. I need to use apply to generalize the solution to work with arbitrary strings with different length.

(defn send-more-money-solutions []
  (run* [s e n d m o r y]
        (fd/in s e n d m o r y (fd/interval 0 9))
        (fd/!= s 0)
        (fd/!= m 0)
        (fd/distinct [s e n d m o r y])
        (fd/eq (= (+ (* 1000 s) (* 100 e) (* 10 n) d
                     (* 1000 m) (* 100 o) (* 10 r) e)
                  (+ (* 10000 m) (* 1000 o) (* 100 n) (* 10 e) y)))))

What should I do? (For above, I have an idea that I could maybe write a macro (although not sure how yet) but actually I need to be able to use variables that is a sequence of logic variables. Something like below)

(fd/eq (= (+ (apply + lvars1) (apply + lvars2))
          (apply + lvars3)))

The error message looks like

java.lang.IllegalArgumentException: Can't call nil, form: (nil + [(* 1000 s) (* 100 e) (* 10 n) d (* 1000 m) (* 100 o) (* 10 r) e] G__1124704)

I think something weird is going on in fd/eq macro so I should try without using eq macro.

Thank you all in advance!

Answer 1

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!)

1. 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)])))
   

2. 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