NAIL094 — Decision procedures and verification

Petr Kučera, KTIML MFF UK

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

Petr Kučera <>