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