haskell

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

However, when dealing with our theorem prover, we are considering Z3 variables, which are addressed as AST nodes. Since Z3 is strictly typed when it comes to booleans vs integers, we'll need two distinct variables jint and jbool. We could make a third auxiliary boolean variable jisbool, that decides which is the case. However, that would make it very tedious to define our constraints as the decision to include j is dynamic. Instead, I decided to make the decision variable a static boolean, expanding our search space to 2 permutations, I think we'll be fine.

{-# 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

In order to count booleans more easily, we'll create a function to convert true to 1 and false to 0:

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

With that we can also create a helper to converts the Integer to an Int in the result of evalInt:

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

full source

Now can finally setup the skeleton for our script. Note that the constraints are still missing.

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

This program just produces a solution with default values as we have not defined any constraints yet:

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

Finally, we run the program and learn in mere milliseconds that we had guessed wrong that j is a boolean answer as the program presents us with a Nothing result. Changing that around produces a solution to our puzzle in a similarly near instantious fashion:

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

SMT solvers truly are the Deus Ex Machina of the puzzle world. The complete project and source can be found at https://github.com/HugoPeters1024/DeductionPuzzle.

last modified: Aug 09, 2023 at 22:20