On 28 April 2014 Gary Antonik had a Numberplay column that quotes my friend Bill Gosper. (Gosper often presents more advanced puzzles in the math-fun mailing list.) This puzzle was:
For the expression
N U M + B E R = P L A Y
,
- Which distinct numerals (each different) can be substituted for letters to make a valid expression?
- How many solutions are there?
I tackled this type of problem (also known as a cryptarithmetic or alphametic or verbal arithmetic problem) in my Udacity class CS 212.
My initial approach follows Ken Thompson's adage, "when in doubt, use brute force."
eval
function to check if the resulting formula is a valid, true expression.The basic idea is simple, but there are a few complications to worry about:
==
for equality and **
for exponentiation, but math notation uses =
and ^
. I'll accept any of these, and translate from math to Python with to_python
.012
) is illegal (except that 0
by itself is ok).1/0
or 4/(3-2-1)
.2 * B or not 2 * BE
, the or
and not
are Python keywords.solve
function to find one solution (faster) or all solutions (comprehensive)? I'll handle both use cases by defining solve
to yield solutions one at a time. You can quickly get the first one with first
or all of them with set
.solve
¶First some imports and type definitions:
from typing import Iterable, Callable, Tuple
from itertools import permutations
import re
Formula = str # A formula in Math notation, like "NUM ^ BER = PLAY"
Pformula = str # A formula in Python notation, like "NUM ** BER == PLAY"
Solution = str # A formula with letters relaced by digits, like "356 + 742 = 1098"
Below we see that solve
works by substituting each permutation of digits for the letters in the formula, and then reporting on the ones that are valid (ones that evaluate to true and have no number with a leading zero). Note that solve
checks if a to_python
version of the formula is valid
, and if it is, returns a substituted version of the original formula.
def solve(formula) -> Iterable[Solution]:
"""Given a formula like 'NUM + BER == PLAY', fill in digits to solve it."""
letters = all_letters(formula)
pformula = to_python(formula)
for digits in permutations('1234567890', len(letters)):
if valid(subst(digits, letters, pformula)):
yield subst(digits, letters, formula)
def subst(digits, letters, formula) -> Formula:
"""Substitute digits for letters in formula."""
return formula.translate(str.maketrans(letters, cat(digits)))
def valid(pformula) -> bool:
"""A pformula is valid iff it has no leading zero, and evaluates to True."""
try:
return (not leading_zero(pformula)) and (eval(pformula) is True)
except ArithmeticError:
return False
def to_python(formula: Formula) -> Pformula:
"""Convert ' = ' and '^' to ' == ' and '**'."""
return formula.replace(' = ', ' == ').replace('^', '**')
def all_letters(formula: str) -> str:
"""The set of letters in formula, in the form of an alphabetized string."""
return cat(sorted(set(re.findall('[A-Z]', formula))))
def first(iterable): "First element"; return next(iter(iterable), None)
cat = ''.join # Function to concatenate strings
leading_zero = re.compile(r'\b0[0-9]').search # Function to check for illegal number
It would be good to have some unit tests for these functions, but I moved them to the end of this notebook, so that we can go right ahead and solve the problem:
first(solve('NUM + BER = PLAY'))
'587 + 439 = 1026'
That's one solution; how many are there all together? And how long does it take to find them?
%time solutions = set(solve('NUM + BER = PLAY'))
len(solutions)
CPU times: user 16.9 s, sys: 19.2 ms, total: 17 s Wall time: 17 s
96
It takes 15 or 20 seconds to find 96 solutions, Here are ten of them:
list(solutions)[:10]
['452 + 637 = 1089', '589 + 437 = 1026', '879 + 426 = 1305', '749 + 286 = 1035', '756 + 342 = 1098', '673 + 425 = 1098', '439 + 587 = 1026', '432 + 657 = 1089', '423 + 675 = 1098', '429 + 876 = 1305']
faster_solve
¶Can we make solve
faster?
To answer the question, I start by profiling to see where the time is spent, using the ipython magic function %prun
:
%prun first(solve('NUM + BER = PLAY'))
3028913 function calls in 3.011 seconds Ordered by: internal time ncalls tottime percall cumtime percall filename:lineno(function) 309270 1.779 0.000 1.833 0.000 {built-in method builtins.eval} 453271 0.229 0.000 0.229 0.000 {method 'translate' of 'str' objects} 453270 0.220 0.000 0.220 0.000 {method 'search' of 're.Pattern' objects} 2 0.215 0.107 3.065 1.532 89248256.py:1(solve) 453271 0.209 0.000 0.669 0.000 89248256.py:9(subst) 453271 0.146 0.000 0.146 0.000 {built-in method maketrans} 453270 0.128 0.000 2.182 0.000 89248256.py:13(valid) 453272 0.084 0.000 0.084 0.000 {method 'join' of 'str' objects} 1 0.000 0.000 3.065 3.065 89248256.py:28(first) 1 0.000 0.000 3.065 3.065 {built-in method builtins.exec} 1 0.000 0.000 0.000 0.000 89248256.py:24(all_letters) 1 0.000 0.000 0.000 0.000 {method 'findall' of 're.Pattern' objects} 1 0.000 0.000 0.000 0.000 re.py:233(findall) 1 0.000 0.000 0.000 0.000 89248256.py:20(to_python) 1 0.000 0.000 0.000 0.000 {built-in method builtins.sorted} 1 0.000 0.000 0.000 0.000 re.py:289(_compile) 1 0.000 0.000 3.065 3.065 {built-in method builtins.next} 1 0.000 0.000 0.000 0.000 {built-in method builtins.isinstance} 2 0.000 0.000 0.000 0.000 {method 'replace' of 'str' objects} 1 0.000 0.000 0.000 0.000 {method 'disable' of '_lsprof.Profiler' objects} 1 0.000 0.000 0.000 0.000 {built-in method builtins.iter} 1 0.000 0.000 0.000 0.000 <string>:1(<module>) 1 0.000 0.000 0.000 0.000 {built-in method builtins.len}
%prun
tells us that over half the time is spent in eval
, which makes sense because we call eval
once for each pemutation of the digits. But we don't need to do that. We could call eval
just once to create a Python function which we than call (not eval) for each permutation. That will be faster, because we won't have to re-eval the formula each time (parsing it and generating bytecode each time); it will be translated once into Python bytecode.
For "NUM + BER = PLAY"
, the Python function could be:
(lambda N,U,M,B,E,R,P,L,A,Y:
N and B and P and (100*N + 10*U + M) + (100*B + 10*E + R) == (1000*P + 100*L + 10*A + Y))
Note that:
NUM
in the math formula translates to (100*N + 10*U + M)
in the Python function.N, B
and P
, cannot be zero, so we test them first.Here is the code to do the translation:
def translate_formula(formula, verbose=False) -> Tuple[str, str]:
"""Translate formula into two values: (lambda function string, parameter letters)."""
letters = all_letters(formula)
assert len(letters) <= 10, f'{len(letters)} letters is too many; only 10 allowed'
firsts = re.findall(r'\b([A-Z])[A-Z]', formula)
body = re.sub('[A-Z]+', translate_word, to_python(formula))
return f'lambda {",".join(letters)}: {" and ".join([*firsts, body])}', letters
def translate_word(matchobj: re.Match) -> str:
"Translate the matched word 'PLAY' to '(((P*10+L)*10+A)*10+Y))', e.g."
word = matchobj.group()
exponents = reversed(range(len(word)))
terms = (f'{10 ** x}*{L}' if x > 0 else L
for x, L in zip(exponents, word))
return '(' + ' + '.join(terms) + ')'
Some usage examples:
translate_formula("A + B = CD")
('lambda A,B,C,D: C and (A) + (B) == (10*C + D)', 'ABCD')
translate_formula("NUM + BER = PLAY")
('lambda A,B,E,L,M,N,P,R,U,Y: N and B and P and (100*N + 10*U + M) + (100*B + 10*E + R) == (1000*P + 100*L + 10*A + Y)', 'ABELMNPRUY')
Now we're ready for the faster version of solve
:
def faster_solve(formula: Formula) -> Iterable[Solution]:
"""Given a formula like 'NUM + BER == PLAY', fill in digits to solve it.
This version precompiles the formula."""
python_lambda, letters = translate_formula(to_python(formula))
formula_fn = eval(python_lambda)
for digits in permutations((1,2,3,4,5,6,7,8,9,0), len(letters)):
try:
if formula_fn(*digits) is True:
yield subst(map(str, digits), letters, formula)
except ArithmeticError:
pass
first(faster_solve('NUM + BER = PLAY'))
'587 + 439 = 1026'
How fast is it?
%time solutions2 = set(faster_solve('NUM + BER = PLAY'))
CPU times: user 1.11 s, sys: 3.16 ms, total: 1.11 s Wall time: 1.11 s
About 15 times faster! Does it give the same solutions as solve
?
assert solutions == solutions2
Yes, it does.
Here are some classic examples as well as some I made up myself:
formulas = """
NUM + BER = PLAY
YOU = ME ^ 2
SEND + MORE = MONEY
FOUR + SCORE + 7 = YEARS + AGO
WRONG + WRONG = RIGHT
WRIGHT + WRIGHT = TO * FLY + FLIGHT
HALF + HALF = WHOLE
HALF + FIFTH + TENTH + TENTH + TENTH = WHOLE
BASE + BALL = GAMES
YOUR + YOU = HEART
EAT + THAT = APPLE
ALPHABET + LETTERS = SCRABBLE
POTATO + TOMATO = PUMPKIN
ODD * ODD = FREAKY
DOUBLE + DOUBLE + TOIL = TROUBLE
WASH + YOUR = HANDS
WEAR + A + MASK + WASH = SAFER
PERSON + WOMAN + MAN = CAMERA
TWO + TWENTY = TWELVE + TEN
AA + BB + CC = ABC
PI * R^2 = AREA
A^2 + B^2 = C^2
A^2 + BE^2 = BY^2
AYH^2 + BEE^2 = SEE^2
RAMN = R^3 + RM^3 = N^3 + RX^3
MON-EY = EVIL^(1/2)
SIN^2 + COS^2 = UNITY
SPEED + LIMIT = FIFTY
TERRIBLE + NUMBER = THIRTEEN
SEVEN + SEVEN + SIX = TWENTY
EIGHT + EIGHT + TWO + ONE + ONE = TWENTY
ELEVEN + NINE + FIVE + FIVE = THIRTY
NINE + SEVEN + SEVEN + SEVEN = THIRTY
FOURTEEN + TEN + TEN + SEVEN = FORTYONE
HAWAII + IDAHO + IOWA + OHIO = STATES
VIOLIN * 2 + VIOLA = TRIO + SONATA
SEND + A + TAD + MORE = MONEY
ZEROES + ONES = BINARY
DCLIZ + DLXVI = MCCXXV
COUPLE + COUPLE = QUARTET
FISH + N + CHIPS = SUPPER
SATURN + URANUS + NEPTUNE + PLUTO = PLANETS
PLUTO not in {PLANETS}
EARTH + AIR + FIRE + WATER = NATURE
TWO * TWO = SQUARE
HIP * HIP = HURRAY
NORTH / SOUTH = EAST / WEST
NAUGHT ^ 2 = ZERO ^ 3
I + THINK + IT + BE + THINE = INDEED
DO + YOU + FEEL = LUCKY
WELL - DO + YOU = PUNK
NOW + WE + KNOW + THE = TRUTH
SORRY + TO + BE + A + PARTY = POOPER
SORRY + TO + BUST + YOUR = BUBBLE
STEEL + BELTED = RADIALS
ABRA + CADABRA + ABRA + CADABRA = HOUDINI
I + GUESS + THE + TRUTH = HURTS
LETS + CUT + TO + THE = CHASE
THATS + THE + THEORY = ANYWAY
TWO + TWO = FOUR
X / X = X
X + X = X
A^N + B^N = C^N and N > 1
ATOM^0.5 = A + TO + M
ALL + GLITTERS is not GOLD
ONE < TWO and FOUR < FIVE
ONE < TWO < THREE < TWO * TWO
(2 * BE or not 2 * BE) = THE + QUES-TION
sum(range(AA)) = BB
sum(range(POP)) = BOBO
ODD + ODD = EVEN
ROMANS+ALSO+MORE+OR+LESS+ADDED = LETTERS
FOUR+ONE = FIVE and ONE+ONE+ONE+ONE+ONE = FIVE
TEN+SEVEN+SEVEN+SEVEN+FOUR+FOUR+ONE = FORTY
NINETEEN+THIRTEEN+THREE+2*TWO+3*ONE = FORTYTWO
IN + ARCTIC + TERRAIN + AN + ANCIENT + EERIE + ICE + TRACT + I + ENTER + A + TRANCE = FLATIANA
ONE < TWO < THREE < SEVEN - THREE < THREE + TWO < THREE + THREE < SEVEN < SEVEN + ONE < THREE * THREE
ABCDEFGHIJ/JIHGFEDCBA = AI/IG
AN + ACCELERATING + INFERENTIAL + ENGINEERING + TALE + ELITE + GRANT + FEE + ET + CETERA = ARTIFICIAL + INTELLIGENCE
""".strip().splitlines()
def show(formulas: Iterable[Formula], sep='_'*90):
"""Solve all the formulas and show results."""
for f in formulas:
print(f'{sep}\n{f}\n{first(faster_solve(f))}')
return len(formulas)
%time show(formulas)
__________________________________________________________________________________________ NUM + BER = PLAY 587 + 439 = 1026 __________________________________________________________________________________________ YOU = ME ^ 2 576 = 24 ^ 2 __________________________________________________________________________________________ SEND + MORE = MONEY 9567 + 1085 = 10652 __________________________________________________________________________________________ FOUR + SCORE + 7 = YEARS + AGO 9071 + 26014 + 7 = 34512 + 580 __________________________________________________________________________________________ WRONG + WRONG = RIGHT 37081 + 37081 = 74162 __________________________________________________________________________________________ WRIGHT + WRIGHT = TO * FLY + FLIGHT 413058 + 413058 = 82 * 769 + 763058 __________________________________________________________________________________________ HALF + HALF = WHOLE 9604 + 9604 = 19208 __________________________________________________________________________________________ HALF + FIFTH + TENTH + TENTH + TENTH = WHOLE 6701 + 14126 + 25326 + 25326 + 25326 = 96805 __________________________________________________________________________________________ BASE + BALL = GAMES 7483 + 7455 = 14938 __________________________________________________________________________________________ YOUR + YOU = HEART 9426 + 942 = 10368 __________________________________________________________________________________________ EAT + THAT = APPLE 819 + 9219 = 10038 __________________________________________________________________________________________ ALPHABET + LETTERS = SCRABBLE 17531908 + 7088062 = 24619970 __________________________________________________________________________________________ POTATO + TOMATO = PUMPKIN 168486 + 863486 = 1031972 __________________________________________________________________________________________ ODD * ODD = FREAKY 677 * 677 = 458329 __________________________________________________________________________________________ DOUBLE + DOUBLE + TOIL = TROUBLE 798064 + 798064 + 1936 = 1598064 __________________________________________________________________________________________ WASH + YOUR = HANDS 5291 + 6748 = 12039 __________________________________________________________________________________________ WEAR + A + MASK + WASH = SAFER 9617 + 1 + 3125 + 9124 = 21867 __________________________________________________________________________________________ PERSON + WOMAN + MAN = CAMERA 320567 + 96817 + 817 = 418201 __________________________________________________________________________________________ TWO + TWENTY = TWELVE + TEN 784 + 781279 = 781351 + 712 __________________________________________________________________________________________ AA + BB + CC = ABC 11 + 99 + 88 = 198 __________________________________________________________________________________________ PI * R^2 = AREA 96 * 7^2 = 4704 __________________________________________________________________________________________ A^2 + B^2 = C^2 3^2 + 4^2 = 5^2 __________________________________________________________________________________________ A^2 + BE^2 = BY^2 5^2 + 12^2 = 13^2 __________________________________________________________________________________________ AYH^2 + BEE^2 = SEE^2 760^2 + 522^2 = 922^2 __________________________________________________________________________________________ RAMN = R^3 + RM^3 = N^3 + RX^3 1729 = 1^3 + 12^3 = 9^3 + 10^3 __________________________________________________________________________________________ MON-EY = EVIL^(1/2) 108-42 = 4356^(1/2) __________________________________________________________________________________________ SIN^2 + COS^2 = UNITY 235^2 + 142^2 = 75389 __________________________________________________________________________________________ SPEED + LIMIT = FIFTY 40221 + 36568 = 76789 __________________________________________________________________________________________ TERRIBLE + NUMBER = THIRTEEN 45881795 + 302758 = 46184553 __________________________________________________________________________________________ SEVEN + SEVEN + SIX = TWENTY 68782 + 68782 + 650 = 138214 __________________________________________________________________________________________ EIGHT + EIGHT + TWO + ONE + ONE = TWENTY 52371 + 52371 + 104 + 485 + 485 = 105816 __________________________________________________________________________________________ ELEVEN + NINE + FIVE + FIVE = THIRTY 797275 + 5057 + 4027 + 4027 = 810386 __________________________________________________________________________________________ NINE + SEVEN + SEVEN + SEVEN = THIRTY 3239 + 49793 + 49793 + 49793 = 152618 __________________________________________________________________________________________ FOURTEEN + TEN + TEN + SEVEN = FORTYONE 19564882 + 482 + 482 + 78082 = 19643928 __________________________________________________________________________________________ HAWAII + IDAHO + IOWA + OHIO = STATES 510199 + 98153 + 9301 + 3593 = 621246 __________________________________________________________________________________________ VIOLIN * 2 + VIOLA = TRIO + SONATA 176478 * 2 + 17645 = 2076 + 368525 __________________________________________________________________________________________ SEND + A + TAD + MORE = MONEY 9283 + 7 + 473 + 1062 = 10825 __________________________________________________________________________________________ ZEROES + ONES = BINARY 698392 + 3192 = 701584 __________________________________________________________________________________________ DCLIZ + DLXVI = MCCXXV 62049 + 60834 = 122883 __________________________________________________________________________________________ COUPLE + COUPLE = QUARTET 653924 + 653924 = 1307848 __________________________________________________________________________________________ FISH + N + CHIPS = SUPPER 5718 + 3 + 98741 = 104462 __________________________________________________________________________________________ SATURN + URANUS + NEPTUNE + PLUTO = PLANETS 127503 + 502351 + 3947539 + 46578 = 4623971 __________________________________________________________________________________________ PLUTO not in {PLANETS} 63985 not in {6314287} __________________________________________________________________________________________ EARTH + AIR + FIRE + WATER = NATURE 67432 + 704 + 8046 + 97364 = 173546 __________________________________________________________________________________________ TWO * TWO = SQUARE 807 * 807 = 651249 __________________________________________________________________________________________ HIP * HIP = HURRAY 958 * 958 = 917764 __________________________________________________________________________________________ NORTH / SOUTH = EAST / WEST 51304 / 61904 = 7260 / 8760 __________________________________________________________________________________________ NAUGHT ^ 2 = ZERO ^ 3 328509 ^ 2 = 4761 ^ 3 __________________________________________________________________________________________ I + THINK + IT + BE + THINE = INDEED 1 + 64125 + 16 + 73 + 64123 = 128338 __________________________________________________________________________________________ DO + YOU + FEEL = LUCKY 57 + 870 + 9441 = 10368 __________________________________________________________________________________________ WELL - DO + YOU = PUNK 5277 - 13 + 830 = 6094 __________________________________________________________________________________________ NOW + WE + KNOW + THE = TRUTH 673 + 38 + 9673 + 128 = 10512 __________________________________________________________________________________________ SORRY + TO + BE + A + PARTY = POOPER 80556 + 20 + 34 + 9 + 19526 = 100145 __________________________________________________________________________________________ SORRY + TO + BUST + YOUR = BUBBLE 94665 + 24 + 1092 + 5406 = 101187 __________________________________________________________________________________________ STEEL + BELTED = RADIALS 87336 + 936732 = 1024068 __________________________________________________________________________________________ ABRA + CADABRA + ABRA + CADABRA = HOUDINI 7457 + 1797457 + 7457 + 1797457 = 3609828 __________________________________________________________________________________________ I + GUESS + THE + TRUTH = HURTS 5 + 26811 + 478 + 49647 = 76941 __________________________________________________________________________________________ LETS + CUT + TO + THE = CHASE 9478 + 127 + 75 + 704 = 10384 __________________________________________________________________________________________ THATS + THE + THEORY = ANYWAY 86987 + 863 + 863241 = 951091 __________________________________________________________________________________________ TWO + TWO = FOUR 734 + 734 = 1468 __________________________________________________________________________________________ X / X = X 1 / 1 = 1 __________________________________________________________________________________________ X + X = X 0 + 0 = 0 __________________________________________________________________________________________ A^N + B^N = C^N and N > 1 3^2 + 4^2 = 5^2 and 2 > 1 __________________________________________________________________________________________ ATOM^0.5 = A + TO + M 1296^0.5 = 1 + 29 + 6 __________________________________________________________________________________________ ALL + GLITTERS is not GOLD 166 + 46500389 is not 4762 __________________________________________________________________________________________ ONE < TWO and FOUR < FIVE 351 < 703 and 2386 < 2491 __________________________________________________________________________________________ ONE < TWO < THREE < TWO * TWO 431 < 674 < 62511 < 674 * 674 __________________________________________________________________________________________ (2 * BE or not 2 * BE) = THE + QUES-TION (2 * 13 or not 2 * 13) = 843 + 7239-8056 __________________________________________________________________________________________ sum(range(AA)) = BB sum(range(11)) = 55 __________________________________________________________________________________________ sum(range(POP)) = BOBO sum(range(101)) = 5050 __________________________________________________________________________________________ ODD + ODD = EVEN 655 + 655 = 1310 __________________________________________________________________________________________ ROMANS+ALSO+MORE+OR+LESS+ADDED = LETTERS 975348+3187+5790+79+1088+36606 = 1022098 __________________________________________________________________________________________ FOUR+ONE = FIVE and ONE+ONE+ONE+ONE+ONE = FIVE 1380+345 = 1725 and 345+345+345+345+345 = 1725 __________________________________________________________________________________________ TEN+SEVEN+SEVEN+SEVEN+FOUR+FOUR+ONE = FORTY 520+12820+12820+12820+4937+4937+902 = 49756 __________________________________________________________________________________________ NINETEEN+THIRTEEN+THREE+2*TWO+3*ONE = FORTYTWO 42415114+56275114+56711+2*538+3*841 = 98750538 __________________________________________________________________________________________ IN + ARCTIC + TERRAIN + AN + ANCIENT + EERIE + ICE + TRACT + I + ENTER + A + TRANCE = FLATIANA 42 + 379549 + 5877342 + 32 + 3294825 + 88748 + 498 + 57395 + 4 + 82587 + 3 + 573298 = 10354323 __________________________________________________________________________________________ ONE < TWO < THREE < SEVEN - THREE < THREE + TWO < THREE + THREE < SEVEN < SEVEN + ONE < THREE * THREE 321 < 483 < 45711 < 91612 - 45711 < 45711 + 483 < 45711 + 45711 < 91612 < 91612 + 321 < 45711 * 45711 __________________________________________________________________________________________ ABCDEFGHIJ/JIHGFEDCBA = AI/IG 1073589264/4629853701 = 16/69 __________________________________________________________________________________________ AN + ACCELERATING + INFERENTIAL + ENGINEERING + TALE + ELITE + GRANT + FEE + ET + CETERA = ARTIFICIAL + INTELLIGENCE 59 + 577404251698 + 69342491650 + 49869442698 + 1504 + 40614 + 82591 + 344 + 41 + 741425 = 5216367650 + 691400684974 CPU times: user 42.1 s, sys: 77.8 ms, total: 42.2 s Wall time: 42.2 s
79
Here are some unit tests for the functions defined above:
for solver in (solve, faster_solve):
assert "1 + 2 = 3" in set(solver("A + B = C"))
assert not set(solver("A + B = CDE"))
assert set(solver("A * B = CA")) == {
'5 * 3 = 15', '5 * 7 = 35', '4 * 6 = 24', '8 * 6 = 48', '2 * 6 = 12', '5 * 9 = 45'}
assert '359 + 847 = 1206' in set(faster_solve('NUM + BER = PLAY'))
assert subst("123", "ABC", "A + B = C") == "1 + 2 = 3"
assert valid("1 + 2 == 3")
assert not valid("1 + 2 == 4")
assert not valid("1/0 == 1/0")
assert to_python("A^B = C") == "A**B == C"
assert all_letters("A + B = C") == "ABC"
assert first("ABC") == "A"
assert cat(['A', 'B', 'C']) == "ABC"
assert leading_zero('012')
assert not leading_zero('123')
assert not leading_zero('0')
assert translate_word(re.match('NUM', 'NUM')) == '(100*N + 10*U + M)'
assert translate_word(re.match('X', 'X')) == '(X)'
assert translate_formula("A + B = CD") == ('lambda A,B,C,D: C and (A) + (B) == (10*C + D)', 'ABCD')
assert translate_formula("NUM + BER = PLAY") == (
'lambda A,B,E,L,M,N,P,R,U,Y: N and B and P and (100*N + 10*U + M) + (100*B + 10*E + R) == (1000*P + 100*L + 10*A + Y)',
'ABELMNPRUY')