In this classic cryptarithm, ten letters stand for the ten decimal digits, each digit used once. Trying every assignment means 3,628,800 permutations. The example instead solves the sum column by column, from right to left, and finds the unique answer with very little search.
Run it in the playground · Source
D O N A L D
+ G E R A L D
= R O B E R T
Find distinct digits for D, O, N, A, L, G, E, R, B, T so that the sum holds, with no leading zero. How many solutions are there?
pandigital_cryptarithm(solution(D, O, N, A, L, G, E, R, B, T)) :-
all_digits(Digits),
% Units: D + D = T, with carry C1.
select(D, Digits, D0),
D \= 0,
UnitsSum is D + D,
T is UnitsSum mod 10,
C1 is UnitsSum // 10,
select(T, D0, D1),
% Tens: L + L + C1 = R, with carry C2.
select(L, D1, D2),
TensSum is L + L + C1,
R is TensSum mod 10,
C2 is TensSum // 10,
R \= 0,
select(R, D2, D3),
...
Each column chooses one new digit with select/3, which also removes it from
the remaining pool, and then computes the result digit and carry instead
of guessing them. Choosing D fixes T; choosing L fixes R.
% Ten-thousands: O cancels, so E + C4 must be exactly 10 * C5.
CarrySum is E + C4,
0 is CarrySum mod 10,
C5 is CarrySum // 10,
% Hundred-thousands: D + G + C5 = R, which derives G directly.
G is R - D - C5,
G > 0,
select(G, D7, D8),
% The sole remaining digit is O; it is also a leading digit.
select(O, D8, []),
O \= 0.
Two columns need no search at all. O appears on both sides of its column, so it cancels; G follows by subtraction; and O is whatever single digit is left.
eyeprolog examples/donald-gerald-robert.pl
pandigital_cryptarithm_answer(naive_search_space, permutations(10, 3628800)).
pandigital_cryptarithm_answer(assignments, solution(5, 2, 6, 4, 8, 1, 9, 7, 3, 0)).
pandigital_cryptarithm_answer(equation, equation(526485, 197485, 723970)).
pandigital_cryptarithm_answer(digit_usage, [5, 2, 6, 4, 8, 1, 9, 7, 3, 0]).
pandigital_cryptarithm_answer(solution_count, 1).
526485 + 197485 = 723970, and it is the only solution.
eyeprolog --proof examples/donald-gerald-robert.pl
step(pandigital_cryptarithm_answer(assignments, solution(5, 2, 6, 4, 8, 1, 9, 7, 3, 0)),
rule(5),
['D' = 5, 'O' = 2, 'N' = 6, 'A' = 4, 'L' = 8, 'G' = 1, 'E' = 9, 'R' = 7, 'B' = 3, 'T' = 0],
[pandigital_cryptarithm(solution(5, 2, 6, 4, 8, 1, 9, 7, 3, 0))]).
The assignment rests on one successful run of the column-by-column solver. Its
proof records every select/3, every mod and // computation, and every
digit test along the way.
eyeprolog --proof examples/donald-gerald-robert.pl > donald-gerald-robert.why.pl
eyeprolog --check-proof donald-gerald-robert.why.pl examples/donald-gerald-robert.pl
condition('C1', resolution, ok, 10).
condition('C4', coverage, ok, 75).
condition('C7', relevance, ok, 72).
obligation(builtin, theory_scoped, countall(pandigital_cryptarithm(A), 1)).
verdict(checked_with_obligations).
The 10 rule steps replay and 56 arithmetic and list steps are recomputed. The claim that there is exactly one solution is an obligation: it counts over the program’s own search, so the checker records it as an assumption rather than proving it.
O \= 0. Does the solution count change?select/3 choices the solver makes, compared with the
3,628,800 permutations of the naive approach.Learn more in The Art of EyeProlog, Chapter 24 (designing finite search).