[kazinator]

I'm trying it with this TXR Lisp, just for fun. It uses an implementation of John MacCarthy's amb operator based on delimited continuations, which are slow.

  (defmacro amb-scope (. forms)
    ^(block amb-scope ,*forms))

  (defun amb (. args)
    (suspend amb-scope cont
      (each ((a args))
        (whenlet ((res (and a (call cont a))))
          (return-from amb-scope res)))))

  (defmacro 0-9 () '(amb 0 1 2 3 4 5 6 7 8 9))

  (defmacro val (p q r) ^(+ (* 100 ,p) (* 10 ,q) ,r))

  (compile-only
    (amb-scope
      (let* ((A (0-9)) (B (0-9)) (C (0-9))
             (D (0-9)) (E (0-9)) (F (0-9))
             (G (0-9)) (H (0-9)) (I (0-9))
             (J (0-9)))
        (amb (and (eql (+ (val A B C)
                          (val D E F)
                          (val G H I))
                       (+ 1230 J))
                  (eql 1023 (mask A B C D E F G H I J))))
        (prinl (list A B C D E F G H I J)))))

Every amb expression says: "I denote my leftmost non-nil argument which makes the remaining computation successful".

The "remaining computation" is the future computation up to returning a value from the enclosing amb-scope form. The amb-scope form succeeds if it yields a non-nil value.

We use amb to ambiguously bind A, B, C, ... to all the values from 0 to 9, amb magically selects the successful value for each one.

We also use amb to express assertions. If we assert (amb (eq 'day 'night)) then that fails: night is not day.

We simply assert the desired conditions over the variables. If there is any way for the conditions to be true, then that means there exist successful values for the variables and so all the prior ambs choose those successful values.

  This is the TXR Lisp interactive listener of TXR 272.
  Quit with :quit or Ctrl-D on an empty line. Ctrl-X ? for cheatsheet.
  Upgrade to TXR Pro for a one-time fee of learning Lisp!
  1> (compile-file "abcprob")
  t
  2> (load "abcprob")
  (0 1 2 3 4 5 8 7 9 6)
  nil

Thus

     012
     345
     879
    ----
    1236

The "all letter digits unique" is efficiently met using bits to represent a set. TXR Lisp has a mask function which calculates an integer whose binary representation has a 1 in the positions indicated by the arguments. E.g (mask 0 2) yields 6, and (mask 0 1 2) yields 7.

If mask is given 10 unique digit values---the complete set---it must produce the value #b1111111111 or 1023, the complete set mask.

We thereby avoid n squared silliness like (and (neql A B) (neql A C) ...): asserting that no letter pair is equal.

[jonsen]

Normally in these kind of cryptogram puzzles the leading digits of a number can't be 0. Your solution has A = 0.

[kazinator]

In that case, we can easily add these constraints to look for another solution, like this --- but that is a poor way:

  (compile-only
    (amb-scope
      (let* ((A (0-9)) (B (0-9)) (C (0-9))
             (D (0-9)) (E (0-9)) (F (0-9))
             (G (0-9)) (H (0-9)) (I (0-9))
             (J (0-9)))
        (amb (and (eql (+ (val A B C)
                          (val D E F)
                          (val G H I))
                       (+ 1230 J))
                  (nzerop A) (nzerop D) (nzerop G) ;; don't do this
                  (eql 1023 (mask A B C D E F G H I J))))
        (prinl (list A B C D E F G H I J)))))

Better just exclude the value 0 from the amb expression for those digits, to reduce the search space:

  (defmacro 0-9 () ^(amb ,*(range 0 9)))

  (defmacro 1-9 () ^(amb ,*(range 1 9)))

  (defmacro val (p q r) ^(+ (* 100 ,p) (* 10 ,q) ,r))

  (compile-only
    (amb-scope
      (let* ((A (1-9)) (B (0-9)) (C (0-9))
             (D (1-9)) (E (0-9)) (F (0-9))
             (G (1-9)) (H (0-9)) (I (0-9))
             (J (0-9)))
        (amb (and (eql (+ (val A B C)
                          (val D E F)
                          (val G H I))
                       (+ 1230 J))
                  (eql 1023 (mask A B C D E F G H I J))))
        (prinl (list A B C D E F G H I J)))))


  1> (compile-file "abcprob.tl")
  t
  2> (load "abcprob")
  (1 0 2 3 4 5 7 8 9 6)

So:

    102
    345
  + 789
  -----
  =1236

:)

[kazinator]

Since we have a math proof that J is 6 in all possible solutions, which works without discovering the other values, we might as well bind (J 6); the purpose is to get the other letters. Binding J cuts down the execution time by close to an order of magnitude.

[kazinator]

John's amb operator has a weakness: it is satisfied with finding one successful value. What if we want all the solutions?

We must invent a related operator. Let us call it kanzen, Japanese for completion/perfection (完全). (This is not the "kan" in "kanren" which is 関連).

amb-scope and amb are defined exactly as before, but we add:

  (defun kanzen (. args)
    (suspend amb-scope cont
      (return-from amb-scope
        (append-each ((a args))
          (whenlet ((res (and a (call cont a))))
            (list res))))))

Using only amb, let's find some pair of integers x y, in the range 0 to 9, whose product is 12:

  (prinl
    (amb-scope
      (let ((x (amb 0 1 2 3 4 5 6 7 8 9))
            (y (amb 0 1 2 3 4 5 6 7 8 9)))
        (amb (eql (* x y) 12))
        (list x y))))

The output is:

  (2 6)

Now, let's change the first amb to kanzen. Just the first one:

  (prinl
    (amb-scope
      (let ((x (kanzen 0 1 2 3 4 5 6 7 8 9))
            (y (amb 0 1 2 3 4 5 6 7 8 9)))
        (amb (eql (* x y) 12))
        (list x y))))

The output now is:

  ((2 6) (3 4) (4 3) (6 2))

all the (x y) pairs are found that multiply to 12.

What does kanzen do differently? Like amb, it cares only about non-nil arguments. However, instead of just finding the first non-nil argument for which the future computation succeeds (returns non-nil), and then returning that result out of amb-scope, kanzen probes all non-nil arguments. It continues the future computation with each value, and for each computation that succeeds (returns non-nil), it collects that value into a list. Then it aborts amb-scope using that list as the result value.

So the weird thing to be understood here is that (list x y) doesn't necessarily determine the ultimate result value of the amb-scope form. The first amb or kanzen call holds the reins, so to speak. If the first operator is amb then, indeed, the result value will be one that was produced by (list x y). amb will try the different futures, and when it finds one that yields non-nil, it aborts amb-scope with that value.

What happens with kanzen is that the ((y (amb ...))) part will find successful y values, and abort amb-scope. But it's doing that aborting within the scope of a continuation created by kanzen, so kanzen intercepts that, collects the (list x y) value, and keeps trying other futures. Thus, confusingly, the result doesn't have shape expected by (list x y).

Note how this is fundamentally hostile to static typing. This code depends on exactly the same piece of syntax, the amb-scope block, having a different type in different contexts: a list of integers during the execution of the search, and a list of lists of integers in the ultimate return.

A static typing theory could be developed for this which assigns multiple types to a node in the program. The interior of amb-scope can see its return value as "pair of integers". all the continuations captured within that scope have that return type. But because of the presence of kanzen, the node can be assigned an external static type as "list of pairs of integers". Or something like that.