## Solving XKCD 287 using Z3 SMT-solver

(The following text has been copypasted to the SAT/SMT by example.)

The problem is to solve the following equation: 2.15a + 2.75b + 3.35c + 3.55d + 4.20e + 5.80f == 15.05, where a..f are integers.

#!/usr/bin/python

from z3 import *

a,b,c,d,e,f = Ints('a b c d e f')
s = Solver()
s.add(215*a + 275*b + 335*c + 355*d + 420*e + 580*f == 1505, a>=0, b>=0, c>=0, d>=0, e>=0, f>=0)

results=[]

# enumerate all possible solutions:
while True:
if s.check() == sat:
m = s.model()
print m
results.append(m)
block = []
for d in m:
c=d()
block.append(c != m[d])
s.add(Or(block))
else:
print "results total=", len(results)
break

There are just 2 solutions:
[f = 0, b = 0, a = 7, c = 0, d = 0, e = 0]
[f = 1, b = 0, a = 1, c = 0, d = 2, e = 0]
results total= 2


Wolfram Mathematica can solve the equation as well:

In[]:= FindInstance[2.15 a + 2.75 b + 3.35 c + 3.55 d + 4.20 e + 5.80 f == 15.05 &&
a >= 0 && b >= 0 && c >= 0 && d >= 0  && e >= 0 && f >= 0,
{a, b, c, d, e, f}, Integers, 1000]

Out[]= {{a -> 1, b -> 0, c -> 0, d -> 2, e -> 0, f -> 1},
{a -> 7, b -> 0, c -> 0, d -> 0, e -> 0, f -> 0}}


1000 means "find at most 1000 solutions", but only 2 are found. See also: http://reference.wolfram.com/language/ref/FindInstance.html.

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.