# Solving newspaper puzzles with SMT solvers

## Puzzle Description

A little while ago, whilst visiting my parents, I was shown a peculiar puzzle in the newspaper in a column by Prof.dr.ir. I. Smeets. It consisted of 10 questions that could either be answered by an integer value, or by true/false. The questions were as follows:

- What is sum of all integer answers?
- How many boolean answers are true?
- Is a the largest number?
- How many integers are equal to me?
- Are all integers positive?
- What is the average of all integers?
- Is d strictly larger than b?
- What is a / h?
- Does f = d - b - h * d hold?
- What is the answer to this question?

Note that the answer to j can be either an integer or true/false.

It quickly becomes apparent that the answers to the questions heavily depend on other questions. Question h is even self referential. Solving this by hand would require some process of deduction and or elimination.

## Attempt to solve it by hand

Note on notation: true = \(\top\) and false = \(\bot\)### Step 1

We can rewrite \(h = a/h\) to \(a = h^2 \). Discovering that h and a do not vary independently.### Step 2

d will always be equal to itself, therefore we can deduce that \( d \ge 1 \)### Step 3

a tells us that \(a = a + b + d + f + h + j? \) (we don't know for sure if j is an integer). The only way for this expression to hold is if all integers except a are 0. But from step 2 we already found that that cannot be the case. Therefore some of the integers must be negative. This allows us to conclude that \(e = \bot \)### Step 4

Divisions cannot yield non integer numbers, thus we know that the sum of all numbers (a) must either be a multiple of 5 or 6, depending on whether j is in integer. In step 1 we also discovered that it must be a square number, leaving not many possibilities.### Step 5

Ugh, I'm stuck.## Brute force the rest?

Given the information we were already able to deduce, we can think of some reasonable ranges for the integer answers to try. After some tweaking and a few minutes of computing time I found the answer by trying the in product of all these ranges, accounting to around 5 million permutations. However I feel too ashamed and too unsatisfied to leave it at that. There has to be a more elegant way that requires a little less luck. (Besides of course actually solving it by hand which is probably very much possible).## Z3, the Deus Ex Machina of puzzles

During a course in my masters program, we had to make a symbolic verifier that attempted to prove whether a program was correct. It did this by taking a fact that should hold at the end of the program, e.g. \( \forall i j : i \lt j : arr[i] \le arr[j] \) for a sorting algorithm It would then go backwards to the program and update whatever constraints on variables needed to hold until it would be at the beginning of the function. At that point you had to use an SMT solver to test if those constraints could be falsified. If so, then you had found an input for which your function would fail, a pretty nifty way to statically test software.

The reason that that is interesting, is because that exposed me to the power of SMT solvers, and specifically taught me how to use Z3. I wondered if I can convert this puzzle into a set of variables and constraints, and find an input for which all the constraints hold, thus generating a solution to the puzzle.

### Modelling the solution datatype

Our final solution object might look something like this.

```
data Solution = Solution
{ a :: Int
, b :: Int
, c :: Bool
, d :: Int
, e :: Bool
, f :: Int
, g :: Bool
, h :: Int
, i :: Bool
, j :: Either Bool Int
} deriving (Show)
```

full source

```
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RecordWildCards #-}
import qualified Z3.Monad as Z
data Z3Solution = Z3Solution
{ a :: Z.AST
, b :: Z.AST
, c :: Z.AST
, d :: Z.AST
, e :: Z.AST
, f :: Z.AST
, g :: Z.AST
, h :: Z.AST
, i :: Z.AST
, jisbool :: Bool
, jint :: Z.AST
, jbool :: Z.AST
} deriving (Show)
mkZ3Solution :: Bool -> Z.Z3 Z3Solution
mkZ3Solution jisbool = Z3Solution
<$> Z.mkFreshIntVar "a"
<*> Z.mkFreshIntVar "b"
<*> Z.mkFreshBoolVar "c"
<*> Z.mkFreshIntVar "d"
<*> Z.mkFreshBoolVar "e"
<*> Z.mkFreshIntVar "f"
<*> Z.mkFreshBoolVar "g"
<*> Z.mkFreshIntVar "h"
<*> Z.mkFreshBoolVar "i"
<*> pure jisbool
<*> Z.mkFreshIntVar "jint"
<*> Z.mkFreshBoolVar "jbool"
getAllBoolsZ3 :: Z3Solution -> [Z.AST]
getAllBoolsZ3 Z3Solution {..} = let bools = [c,e,g,i] in if jisbool then jbool:bools else bools
getAllIntsZ3 :: Z3Solution -> [Z.AST]
getAllIntsZ3 Z3Solution {..} = let ints = [a,b,d,f,h] in if jisbool then ints else jint:ints
```

full source### Some auxiliary Z3 helpers

Z3 does not care about divisions resulting in something other than an integer, and just rounds down to the nearest one. Since we do care, we create the following helper function:

```
mkIntDiv :: Z.AST -> Z.AST -> Z.Z3 Z.AST
mkIntDiv lhs rhs = do
-- Assert that the divider is not zero
Z.assert =<< Z.mkNot =<< Z.mkEq rhs =<< Z.mkInteger 0
-- Assert that lhs % rhs == 0
Z.assert =<< uncurry Z.mkEq =<< (,) <$> Z.mkMod lhs rhs <*> Z.mkInteger 0
-- Proceed with the division
Z.mkDiv lhs rhs
```

full source

```
boolToInt :: Z.AST -> Z.Z3 Z.AST
boolToInt v = do
_0 <- Z.mkInteger 0
_1 <- Z.mkInteger 1
Z.mkIte v _1 _0
```

full source### The main script

With the boilerplate boiling, we can setup our z3 universe. This will be a script that might produce a solution. We can get this solution by evaluating the integers and booleans and combining in them in our previously defined Solution datatype. The problem is however that the evaluation functions produce a value of type Z3 (Maybe a). This means that using a traditional Functor and Applicative approach won't cut it because we'd be propagating (Maybe a) instead. What we actually want is a version of fmap and ap that operates on a nested structure:

```
(<$$>) :: (Functor f1, Functor f2) => (a -> b) -> f1 (f2 a) -> f1 (f2 b)
f <$$> arg = fmap (fmap f) arg
(<**>) :: (Monad a1, Monad a2) => a1 (a2 (a -> b)) -> a1 (a2 a) -> a1 (a2 b)
f <**> arg = f >>= \f -> arg >>= \arg -> pure (ap f arg)
```

full source

```
evalInt' :: Z.Model -> Z.AST -> Z.Z3 (Maybe Int)
evalInt' m v = fromIntegral <$$> Z.evalInt m v
```

full source

```
solve :: Z.Z3 (Maybe Solution)
solve = do
-- For now we assume that j is in fact a boolean answer
sol@Z3Solution {..} <- mkZ3Solution True
-- THIS IS WHERE THE CONSTRAINTS WILL BE
-- eval the values
fmap (fmap fromJust . snd) $ Z.withModel $ \m -> Solution
<$$> evalInt' m a
<**> evalInt' m b
<**> Z.evalBool m c
<**> evalInt' m d
<**> Z.evalBool m e
<**> evalInt' m f
<**> Z.evalBool m g
<**> evalInt' m h
<**> Z.evalBool m i
<**> if jisbool then Left <$$> Z.evalBool m jbool else Right <$$> evalInt' m jint
main :: IO ()
main = Z.evalZ3 solve >>= print
```

full source

```
Just (Solution {a = 0, b = 0, c = False, d = 0, e = False, f = 0, g = False, h = 0, i = False, j = Left False})
```

### The constraints

Now all that is left, is modelling the questions as constraints.

```
_0 <- Z.mkInteger 0
_1 <- Z.mkInteger 1
let ints = getAllIntsZ3 sol
let numints = length ints
let bools = getAllBoolsZ3 sol
boolints <- mapM boolToInt bools
-- a is the sum of ints
Z.assert =<< Z.mkEq a =<< Z.mkAdd ints
-- b is the number of trues
Z.assert =<< Z.mkEq b =<< Z.mkAdd boolints
-- c is wether a is the largest
Z.assert =<< Z.mkEq c =<< Z.mkAnd =<< mapM (Z.mkGe a) ints
-- d is how many are equal to me
Z.assert =<< Z.mkEq d =<< Z.mkAdd =<< mapM (Z.mkEq d >=> boolToInt) ints
-- e is whether all integers are positive
Z.assert =<< Z.mkEq e =<< Z.mkAnd =<< mapM (Z.mkLe _0) ints
-- f is the average of all ints
Z.assert =<< Z.mkEq f =<< mkIntDiv a =<< Z.mkInteger (fromIntegral numints)
-- g is d>b
Z.assert =<< Z.mkEq g =<< Z.mkGt d b
-- h is a/h
Z.assert =<< Z.mkEq h =<< mkIntDiv a h
-- i is f == d - b - h * d
htimesd <- Z.mkMul [h,d]
Z.assert =<< Z.mkEq i =<< Z.mkEq f =<< Z.mkSub [d,b,htimesd]
```

full source

```
Just (Solution {a = 144, b = 2, c = True, d = 2, e = False, f = 24, g = False, h = -12, i = True, j = Right (-16)})
```