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