Computers can help to solve non-trivial problems (e.g. scheduling, optimization, software verification) by automatically deriving models that satisfy sets of constraints. This is called *reasoning with computer support* or *automated reasoning*. There are various tools on the market that can be applied; I will be using Microsoft's Z3 theorem prover. In this blog post, I will be solving a logic puzzle with Z3. The puzzle consists of a set of constraints that a solution must satisfy.

## Zebra puzzle

The zebra puzzle (also known as "Einstein's puzzle", although there is no proof of Einstein being the author) consists of 15 rules involving 5 people, 5 houses, 5 pets, 5 drinks and 5 brands of cigarettes. The cigarettes are not used in more politically correct versions of the puzzle. The rules are as follows:

- The British person lives in the red house.
- The Swede keeps dogs as pets.
- The Dane drinks tea.
- The green house is on the left of the white house.
- The green homeowner drinks coffee.
- The man who smokes Pall Mall keeps birds.
- The owner of the yellow house smokes Dunhill.
- The man living in the center house drinks milk.
- The Norwegian lives in the first house.
- The man who smokes Blend lives next to the one who keeps cats.
- The man who keeps the horse lives next to the man who smokes Dunhill.
- The man who smokes Bluemaster drinks beer.
- The German smokes Prince.
- The Norwegian lives next to the blue house.
- The man who smokes Blend has a neighbor who drinks water.

The question is: *who owns the zebra?*. We can use a theorem prover to answer this question. In order to do this, we need to first come up with a representation of these constraints in logical terms. Each nationality, pet, house color, cigarette brand and drink is associated with a house number (1 through 5) for which we construct a variable. Notice that that this representation is convenient for expressing constraints (4), (9), (14) and (15). We have 5 sets of variables that can be indexed (arrays/lists):

Assume that describes all variables.

### Basic constraints

Before we begin with the 15 rules, we need to make sure that some implicit constraints are expressed.

**Each variable is associated with a house 1 through 5**

**All variables in each category refer to different houses**

. Then we have the following constraints: , , , and .

### Rules

*The British person lives in the red house.*

*The Swede keeps dogs as pets.*

*The Dane drinks tea.*

*The green house is on the left of the white house.*

*The green homeowner drinks coffee.*

*The man who smokes Pall Mall keeps birds.*

*The owner of the yellow house smokes Dunhill.*

*The man living in the center house drinks milk.*

*The Norwegian lives in the first house.*

*The man who smokes Blend lives next to the one who keeps cats.*

*The man who keeps the horse lives next to the man who smokes Dunhill.*

*The man who smokes Bluemaster drinks beer.*

*The German smokes Prince.*

*The Norwegian lives next to the blue house.*

*The man who smokes Blend has a neighbor who drinks water.*

## Feeding Z3

Now that we have a representation, we can feed it to Z3. The tool is available here. Create a F# project and add a reference to "Microsoft.Z3.dll" so that we can use the API. We start with the definition of the Z3 context. Make sure you have opened the Microsoft.Z3 namespace and add the following line:

```
let context = new Context()
```

Now, let us add the sets in the form of lists:

```
let Nat = ["brit"; "swede"; "dane"; "norwegian"; "german"]
let Col = ["red"; "white" ;"green";"yellow";"blue"]
let Pet = ["dogs"; "birds"; "horses"; "cats";"fish"]
let Drk = ["tea";"beer";"coffee";"water";"milk"]
let Smk = ["pallmall";"dunhill";"blends";"prince";"bluemasters"]
let V = Nat @ Col @ Pet @ Drk @ Smk
```

In order to use these variables, we need to define them in the Z3 context. Define a dictionary that maps names to variable references, where each variable is of type integer:

```
//the body of vars is only evaluated once
let vars = V |> List.map ( fun v -> (v, context.MkConst(v, context.MkIntSort())) ) |> dict
```

Construct the "diff" function; it returns a term that represents a constraint:

```
let diff lst =
let constr = [|for v in lst do
let cs = [|for v' in lst do if v' <> v then yield context.MkNot(context.MkEq(vars.[v], vars.[v']))|]
yield context.MkAnd(cs)
|]
context.MkAnd(constr)
```

Note that a chain of conjunctions is constructed, which is equivalent to the universal quantifier we used in diff.

Also, we define a helper function to construct an integer constant and a function to define a "neighbor" constraint term:

```
let mkInt (n:int) = context.MkIntNumeral(n)
//is x a neighbor of y
let isNeighborOf x y = context.MkOr(context.MkEq(vars.[x], context.MkSub(vars.[y], mkInt 1)),
context.MkEq(vars.[x], context.MkAdd(vars.[y], mkInt 1))
)
```

Define the constraint that all variables range between 1 and 5:

```
let rangeConstr =
let constr = vars |> Seq.map ( fun kv ->
context.MkAnd(context.MkGt(kv.Value, mkInt 0), context.MkLt(kv.Value, mkInt 6))
)
context.MkAnd(Array.ofSeq constr)
```

Define the constraint that all variables in a set point to different houses:

```
let allDiff = context.MkAnd(
[|
diff Nat;
diff Col;
diff Pet;
diff Drk;
diff Smk
|])
```

Now define all the game rules:

```
let isEqual x y = context.MkEq(vars.[x], vars.[y])
//The Brit lives in the red house
let constr1 = isEqual "brit" "red"
//The Swede keeps dogs as pets.
let constr2 = isEqual "swede" "dogs"
//The Dane drinks tea.
let constr3 = isEqual "dane" "tea"
//The green house is on the left of the white house.
let constr4 = context.MkEq(vars.["green"], context.MkSub(vars.["white"], mkInt 1))
//The green house's owner drinks coffee.
let constr5 = isEqual "green" "coffee"
//The person who smokes Pall Mall rears birds.
let constr6 = isEqual "pallmall" "birds"
//The owner of the yellow house smokes Dunhill.
let constr7 = isEqual "yellow" "dunhill"
//The man living in the center house drinks milk.
let constr8 = context.MkEq(vars.["milk"], mkInt 3)
//The Norwegian lives in the first house.
let constr9 = context.MkEq(vars.["norwegian"], mkInt 1)
//The man who smokes Blends lives next to the one who keeps cats.
let constr10 = isNeighborOf "blends" "cats"
//The man who keeps the horse lives next to the man who smokes Dunhill.
let constr11 = isNeighborOf "horses" "dunhill"
//The owner who smokes Bluemasters drinks beer.
let constr12 = isEqual "bluemasters" "beer"
//The German smokes Prince.
let constr13 = isEqual "german" "prince"
//The Norwegian lives next to the blue house.
let constr14 = isNeighborOf "norwegian" "blue"
//The man who smokes Blends has a neighbor who drinks water.
let constr15 = isNeighborOf "water" "blends"
```

Combine all the constraints we defined in one term:

```
let puzzle = context.MkAnd([|allDiff; rangeConstr; constr1; constr2; constr3; constr4; constr5; constr6; constr7; constr8; constr9;constr10;
constr11; constr12; constr13; constr14; constr15|])
```

Now ask Z3 for a model that satisfies our constraints:

```
let program =
let _ = context.AssertCnstr(puzzle)
let model:Model ref = ref null
let result = context.CheckAndGetModel(model)
if result = LBool.True then model.Value.Display(System.Console.Out)
```

In the model, zebra and german have the value 4 (4th house). Therefore, the german has the zebra.