home

Numerical Riddles and SAT Solvers

2017-11-07

Regarding a riddle meme that went around on Facebook...

Little known tidbit of computer science: this is a generally solved problem.

Using the Z3 solver from Microsoft (available at https://rise4fun.com/z3), I encode the riddle as follows:

` (declare-const n-gon Int) (declare-const bananna Int) (declare-const clock Int) (declare-const question Int) (assert ( = 45 (+ n-gon n-gon n-gon))) (assert ( = 23 (+ bananna bananna n-gon))) (assert ( = 10 (+ bananna clock clock))) (assert ( = question (+ clock bananna (* bananna n-gon)))) (check-sat)

(get-model) `

I run the above code and get informed that the riddle is satisfiable (not all equations are satisfiable), along with a breakdown of some integers that satisfy it.

` sat (model (define-fun question () Int 67) (define-fun clock () Int 3) (define-fun bananna () Int 4) (define-fun n-gon () Int 15)

)

`

Suppose you have a modelling problem that is encodable as a system of equations - the Z3 solver (a member of the set of SMT solvers) can address this problem for you. Examples here can include sales models, test choices for equipment, proper component alignment for manufacturing, etc. List can go on for a while. These are useful tools.