Cryptarithms [5 points]
Cryptarithms (also Alphametics) is a number puzzle. An alphabet is used to encode some numbers of base \(k\). The goal is to form a one-to-one function between the alphabet and the numbers so that the decoded mathematical formula is satisfied. The size of the alphabet is bounded by \(k\). Numbers cannot have leading zeros. A famous example of Cryptarithms (with \(k=10\)) along with its solution is
SEND 9567
+MORE +1085
----- -----
MONEY 10652
Use SAT/SMT solvers to solve cryptarithms, an extended description of what is expected follows.
Extended description
The basic constraint we allow is an equation \[ w_1 \operatorname{\square} w_2 \operatorname{\square} \dots \operatorname{\square} w_n = s \] where \(w_i\), \(i=1, ..., n\) and \(s\) are words and \(\operatorname{\square}\) represent an operator of addition or subtraction. The first letter in a word is never \(0\). The problem consists of a formula which uses the above equation constraints as atoms, e.g. \[ (\mathtt{SEND} + \mathtt{MORE} = \mathtt{MONEY}) \lor (\mathtt{SQUARE} - \mathtt{DANCE} = \mathtt{DANCER}) \]
When reading the input, you can use ||
or OR
to denote a disjunction, &&
or AND
to denote a conjunction, and NOT
to denote a negation (or pick another reasonable format).
- Make unique interpretation of characters as digits optional (i.e. allow also the case when two characters can represent the same digits.
- Check if the solution is unique, count or enumerate all solutions (as an option).
- Try to solve some of the instances from this page (try also more complex formulas which use these equations).
- How long does it take to solve the following problem? \[ \begin{aligned} &\mathtt{SO}+\mathtt{MANY}+\mathtt{MORE}+\mathtt{MEN}+\mathtt{SEEM}+\mathtt{TO}+\mathtt{SAY}+\mathtt{THAT}+\\\\ &\mathtt{THEY}+\mathtt{MAY}+\mathtt{SOON}+\mathtt{TRY}+\mathtt{TO}+\mathtt{STAY}+\mathtt{AT}+\mathtt{HOME}+\\\\ &\mathtt{SO}+\mathtt{AS}+\mathtt{TO}+\mathtt{SEE}+\mathtt{OR}+\mathtt{HEAR}+\mathtt{THE}+\mathtt{SAME}+\mathtt{ONE}+\\\\ &\mathtt{MAN}+\mathtt{TRY}+\mathtt{TO}+\mathtt{MEET}+\mathtt{THE}+\mathtt{TEAM}+\mathtt{ON}+\mathtt{THE}+\\\\ &\mathtt{MOON}+\mathtt{AS}+\mathtt{HE}+\mathtt{HAS}+\mathtt{AT}+\mathtt{THE}+\mathtt{OTHER}+\mathtt{TEN}\\\\ &=\mathtt{TESTS} \end{aligned} \]