Verbal Arithmetic In Rust And Z3

I've been trying to learn Rust on again and off again for the past few months. To motivate myself, I wanted to fool around a bit with Z3 (an SMT solver) in Rust. This quickly turned into quite a bit of a struggle, as while there are Rust bindings available, I'm finding them fairly difficult to work with. I'm not sure if this difficulty stems from the bindings being unergonomic, or that my Rust knowledge is still too basic.

Furthermore, I also haven't been able to find any good, accessible examples of simple toy problems modelled in Z3 using Rust. This post aims to kill two birds with one stone, and presents a simple implementation of a "verbal arithmetic" solver! Hopefully, I'll be able to turn it into a series of examples. :-) (Disclaimer: my Rust knowledge is still pretty basic -- the implementation shown below will most likely pretty naive. You have been warned!)

Verbal Arithmetic

Verbal arithmetic, also known as cryptarithmetic, is a math puzzle in which you are given a mathematical equation consisting of words instead of numbers. To solve it, you need to assign a digit to each letter of the puzzle so that the equation is correct. More concretely, the rules are as follows:

• Each letter should be assigned a digit (0-9).
• Different letters cannot have the same digit.
• The first letter of each word cannot be zero.

A common example of a puzzle is "SEND + MORE = MONEY":

  SEND
+ MORE
 -----
 MONEY

Modeling the puzzle in z3.rS

First, we need to import z3.rs and initialize our solver. Creating a solver consists of a few steps.

use z3::*;
use z3::ast::Ast;

fn main() {
    let config = Config::new();
    let ctx = Context::new(&config);
    let solver = Solver::new(&ctx);

    cryptarithmetic(&solver, &ctx);
}

Now we can start to model the actual puzzle. The first thing we'll need is a way to represent each letter of the puzzle. Since these are integer numbers, we introduce an Int constant for each letter. Below is probably not the most efficient way to create these letters, but it works in a pinch.

fn cryptarithmetic(solver: &Solver, ctx: &Context) {
    let s = ast::Int::new_const(&ctx, "S");
    let e = ast::Int::new_const(&ctx, "E");
    let n = ast::Int::new_const(&ctx, "N");
    let d = ast::Int::new_const(&ctx, "D");
    let m = ast::Int::new_const(&ctx, "M");
    let o = ast::Int::new_const(&ctx, "O");
    let r = ast::Int::new_const(&ctx, "R");
    let y = ast::Int::new_const(&ctx, "Y");

In SMT, numerical variables have no upper or lower bound: they can represent any number between negative infinity and positive infinity. While this is a great property for many applications, our digits can only represent a value between 0 and 9. To enforce this constraint, we can add assertions to the Z3 solver. (At the time of writing, i32 is not yet supported in comparisons so we can't write 0/1/9 directly. To overcome this, we first create an Int representing them.)

let zero = ast::Int::from_i64(&ctx, 0);
let one = ast::Int::from_i64(&ctx, 1);
let nine = ast::Int::from_i64(&ctx, 9);

solver.assert(&s.ge(&one));
solver.assert(&s.le(&nine));
solver.assert(&e.ge(&zero));
solver.assert(&e.le(&nine));
solver.assert(&n.ge(&zero));
solver.assert(&n.le(&nine));
solver.assert(&d.ge(&zero));
solver.assert(&d.le(&nine));
solver.assert(&m.ge(&one));
solver.assert(&m.le(&nine));
solver.assert(&o.ge(&zero));
solver.assert(&o.le(&nine));
solver.assert(&r.ge(&zero));
solver.assert(&r.le(&nine));
solver.assert(&y.ge(&zero));
solver.assert(&y.le(&nine));

Now that we are sure that each letter will contain an appropriate digit, we can focus on the second rule of the puzzle: two digits cannot have the same value. While we could explicitly type this out for each combination of two letters, there's a much easier way in Z3: the distinct assertion! Indeed, given a set of variables, it will ensure that none of the variables have the same value.

solver.assert(&ast::Ast::distinct(&ctx, &[&s, &e, &n, &d, &m, &o, &r, &y]));

Finally, we can encode the actual equation. This is actually quite straightforward -- see for yourself:

let ten = ast::Int::from_i64(&ctx, 10);
let hundred = ast::Int::from_i64(&ctx, 100);
let thousand = ast::Int::from_i64(&ctx, 1000);
let tthousand = ast::Int::from_i64(&ctx, 10000);

let send = &s * &thousand + &e * &hundred + &n * &ten + &d;
let more = &m * &thousand + &o * &hundred + &r * &ten + &e;
let money = &m * &tthousand + &o * &thousand + &n * &hundred + &e * &ten + &y;

solver.assert(&money._eq(&(&send + &more)));

And that's it! We can now have Z3 check for a solution, and then request the model if its available. This will give us the answer to the puzzle.

match solver.check() {
    SatResult::sat => println("{}", solver.get_model().unwrap()), 
    _ => println!("No solution found."),
}

S -> 9
E -> 5
N -> 6
D -> 7
M -> 1
O -> 0
R -> 8
Y -> 2