Solving logic puzzles with F# and Z3

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:

  1. The British person lives in the red house.
  2. The Swede keeps dogs as pets.
  3. The Dane drinks tea.
  4. The green house is on the left of the white house.
  5. The green homeowner drinks coffee.
  6. The man who smokes Pall Mall keeps birds.
  7. The owner of the yellow house smokes Dunhill.
  8. The man living in the center house drinks milk.
  9. The Norwegian lives in the first house.
  10. The man who smokes Blend lives next to the one who keeps cats.
  11. The man who keeps the horse lives next to the man who smokes Dunhill.
  12. The man who smokes Bluemaster drinks beer.
  13. The German smokes Prince.
  14. The Norwegian lives next to the blue house.
  15. 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):

 \begin{array}{l} Nat = \{\text{brit}, \text{swede}, \text{dane}, \text{norwegian}, \text{german}\} \\ Col = \{\text{red}, \text{white}, \text{green}, \text{yellow}, \text{blue}\} \\ Pet = \{\text{dogs}, \text{birds}, \text{horses}, \text{cats}, \text{zebra}\} \\ Drk = \{\text{tea}, \text{beer}, \text{coffee}, \text{water}, \text{milk}\} \\ Smk = \{\text{pallmall}, \text{dunhill}, \text{blends}, \text{prince}, \text{bluemasters}\} \end{array}

Assume that V = Nat \cup Col \cup Pet \cup Drk \cup Smk 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

\forall x \in V. 1 \leq x \leq 5

All variables in each category refer to different houses

 \text{diff}(S) \mathrel{\mathop:}= \forall (i, j) \in \{1, \cdots, 5\}^2. i \neq j \implies S_i \neq S_j

. Then we have the following constraints: \text{diff}(Nat), \text{diff}(Col), \text{diff}(Pet), \text{diff}(Drk) and \text{diff}(Smk).

Rules

  • The British person lives in the red house.

     \text{brit} = \text{red}

  • The Swede keeps dogs as pets.

     \text{swede} = \text{dogs}

  • The Dane drinks tea.

     \text{dane} = \text{tea}

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

     \text{green} = \text{white} - 1

  • The green homeowner drinks coffee.

     \text{green} = \text{coffee}

  • The man who smokes Pall Mall keeps birds.

     \text{pallmall} = \text{birds}

  • The owner of the yellow house smokes Dunhill.

     \text{yellow} = \text{dunhill}

  • The man living in the center house drinks milk.

     \text{milk} = 3

  • The Norwegian lives in the first house.

     \text{norwegian} = 1

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

     (\text{blend} = \text{cats} - 1) \vee (\text{blend} = \text{cats} + 1)

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

     (\text{horse} = \text{dunhill} - 1) \vee (\text{horse} = \text{dunhill} + 1)

  • The man who smokes Bluemaster drinks beer.

     \text{bluemaster} = \text{beer}

  • The German smokes Prince.

     \text{german} = \text{prince}

  • The Norwegian lives next to the blue house.

     (\text{norwegian} = \text{blue} - 1) \vee (\text{norwegian} = \text{blue} + 1)

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

     (\text{water} = \text{blend} - 1) \vee (\text{water} = \text{blend} + 1)

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.

Model based testing with F#, C# and JTorX

Model based testing can be applied to rigorously test software modules. The basic concept is that there is some specification (a model) and an implementation (can be a model or a piece of software). The implementation is regarded as a black box, also known as system under test (SUT). In this post, I'll give a very simple example of a situation where this technique can be applied. I'll be using JTorX as a tool for testing.

Consider a simple coffee machine. Fill it up with some water, fill the pod with some coffee beans, press a button and enjoy a cup of coffee.

It is possible to model such a process with a mealy machine. The following model could be an accurate description of a coffee machine:

According to the model, the machine has at least the following properties:

  • Pressing the coffee button before inserting both water and coffee beans will result in failure.
  • When the coffee machine has failed, the only way to reset it is to clean it.

We model the coffee machine as a set of states (the circles in the picture), where each state resembles some possible state of the coffee machine. We consider a to be the initial state. The machine can transition to another state because of user input (e.g. a user pressed a button). Each input also triggers an output: the coffee machine is capable of reporting "Ok", "Fail" and it should be able to output some coffee. Each edge in the graph is of the form "input / output". The idea is that this model is a specification of the behaviour we expect from a system that is considered to be a coffee machine. It's possible to use this specification for testing. We will use the ioco (input-output conformance) relation defined on labelled transition systems to make this happen. I will not go deeply into this theory, everything is explained in detail in the paper "Model Based Testing With Labelled Transition Systems" by Tretmans.

In order to use ioco, we need to convert the mealy machine to a labelled transition system (LTS). In essence, the main difference is that each transition (edge) of a LTS describes precisely one output or input. The mealy machine describes both an input and output for each transition. We can easily convert each transition from the mealy machine to a LTS using this conversion tactic:

Unfortunately, the resulting LTS model is not quite as readable:

Now that we have a LTS, we can use the ioco relation to test implementations for conformance. This is done by testing each "trace" of the specification (the LTS) with the implementation to see if the output conforms with the output that is allowed by the specification. A trace is a path from one state p in the graph to another state q:  p \xrightarrow{a} q, where a is some output or input. It can be empty (\epsilon) or it can be quiescent, but we will not go in detail about that here.  p \xrightarrow{a . b} q is shorthand for  p \xrightarrow{a} q' \xrightarrow{b} q . An example trace of the LTS model is  a \xrightarrow{?water . !ok . ?pod . !ok . ?button } h. ioco requires that all possible outputs of the implementation after a trace are foreseen by the specification. Formally, this is defined by  \forall s \in \text{Straces}(\text{spec}). \ out(\text{impl} \ \textbf{after} \ s) \subseteq out(\text{spec} \ \textbf{after} \ s) . We have that out(spec \ \textbf{after} \ \text{?water . !ok . ?pod . !ok . ?button}) = \{ \text{!coffee} \}, if a = \ \text{spec}. This means that an implementation cannot output tea after we press the button on the coffee machine. However, if the trace is not defined by the specification, the implementation can define any behaviour it desires for that particular trace. This means that the trace is underspecified. For more information about ioco, please take a look at the paper I referenced earlier.

Now let's define a simple implementation of a coffee machine in F#:


module Machine

type States  = A | B | C | D | E | F

type Inputs  = Pod | Clean | Water | Button

type Outputs = Fail | Ok | Coffee

type State   = States

let transitionFunc = dict [
                            (A, Clean),  (A, Ok);
                            (A, Pod),    (B, Ok);
                            (A, Button), (F, Fail);
                            (A, Water),  (C, Ok);
                            (B, Pod),    (B, Ok);
                            (B, Clean),  (A, Ok);
                            (B, Button), (F, Fail);
                            (B, Water),  (D, Ok);
                            (C, Pod),    (D, Ok);
                            (C, Clean),  (A, Ok);
                            (C, Water),  (C, Ok);
                            (C, Button), (F, Fail);
                            (D, Pod),    (D, Ok);
                            (D, Clean),  (A, Ok);
                            (D, Water),  (D, Ok);
                            (D, Button), (E, Coffee);
                            (E, Clean),  (A, Ok);
                            (E, Button), (F, Fail);
                            (E, Water),  (F, Fail);
                            (E, Pod),    (F, Fail);
                            (F, Clean),  (A, Ok);
                            (F, Button), (F, Fail);
                            (F, Water),  (F, Fail);
                            (F, Pod),    (F, Fail);
                          ]

let coffeeMachine input state = 
        let success, result = transitionFunc.TryGetValue((state, input))
        if success then Some(result) else None
    
let initialState = A

The main definition in the code above is the function transitionFunc : State \times Input \rightarrow State \times Output, which is modeled as a set. Given some state and input, it will return the associated next state and output if present. We would like to test this implementation using the specification defined earlier. In order to do this, we need some way to communicate with the above program (system under test). Therefore, we construct a simple C# application that is able to communicate through sockets:


using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using System.Net.Sockets;
using System.Text;
using System.Net;
using Microsoft.FSharp.Core;

namespace CoffeeMachine
{
    class Program
    {
        static void Main(string[] args)
        {
            StartServer(5000);
        }

        static void StartServer(int port)
        {
            var server = new TcpListener(IPAddress.Any, port);

            server.Start();

            while ( true )
            {
                var client = server.AcceptTcpClient();

                HandleClient(client);

                client.Close();
            }
        }

        static void HandleClient(TcpClient client)
        {
            var networkStream = client.GetStream();
            var state = Machine.initialState;
            var outputs = new Dictionary<Machine.Outputs, string>()
            {{Machine.Outputs.Coffee, "!coffee"}, {Machine.Outputs.Fail, "!fail"}, {Machine.Outputs.Ok, "!ok"}};

            var inputs = new Dictionary<string, Machine.Inputs>() {
                {"?button", Machine.Inputs.Button},
                {"?pod", Machine.Inputs.Pod},
                {"?clean", Machine.Inputs.Clean},
                {"?water", Machine.Inputs.Water},
            };

            var states = new Dictionary<Machine.States, string>() {
                {Machine.States.A, "A"},
                {Machine.States.B, "B"},
                {Machine.States.C, "C"},
                {Machine.States.D, "D"},
                {Machine.States.E, "E"},
                {Machine.States.F, "F"},
            };

            using (StreamWriter writer = new StreamWriter(networkStream))
            {
                using (StreamReader reader = new StreamReader(networkStream))
                {
                    string inputStr = string.Empty;
                    while ((inputStr = reader.ReadLine()) != null)
                    {
                        Machine.Inputs input = null;
                        if (inputs.TryGetValue(inputStr, out input))
                        {
                            var output = Machine.coffeeMachine(input, state);
                            
                            if (FSharpOption<Tuple<Machine.States, Machine.Outputs>>.get_IsSome(output))
                            {
                                Console.WriteLine("read {0}, output: {1}. new state: {2}", inputStr,
                                    outputs[output.Value.Item2], states[output.Value.Item1]);

                                state = output.Value.Item1;
                                writer.WriteLine(outputs[output.Value.Item2]);
                                writer.Flush();
                            }
                        }
                        else
                        {
                            Console.WriteLine("do not understand {0}", inputStr);
                        }
                    }
                }
            }
        }
    }
}

The above program accepts connections and routes inputs to the coffee machine we've defined in F#. Now we can use JTorX to test the implementation:

Configure JTorX such that it will communicate with our SUT using sockets (select the proper option for "implementation"). Then enter "localhost!5000" to configure the endpoint. Now that it is configured, it is possible to let JTorX test the implementation. Press the start button on the "Test" tab. Then press "Auto". JTorX will happily traverse the LTS model and test each path with the implementation. When each path is covered, you can stop the test process by clicking the "Stop" button. A message sequence chart and coverage analysis is maintained during testing.

Of course, the coffee machine is an extremely trivial example. More complex examples include protocol specifications or parts of larger systems that can be expressed with state machines.

Semantics in F# (utilizing combinators)

Functional languages are convenient for defining semantics of programming languages. In this post, I'll show an example of such a semantic in F# for a simple programming language. I will also show how some combinators can help to produce readable code.

Given the grammar:


expr  := var | number | bool | expr + expr | expr - expr | expr * expr | expr == expr | expr /\ expr | !expr 
stmnt := var = expr; |  if ( expr ) stmnt [else stmnt] | { stmnt+ } | while ( expr ) stmnt

Let's define the following f# data structures:


type Op = Plus | Subtr | Div | Mul | Eq | And | Not

type Expr =
| Variable of string
| Int of int
| Bool of bool
| BinOp of Op * Expr * Expr
| UnOp of Op * Expr

type Statement =
| Block of list<Statement>
| If of Expr * Statement * option<Statement>
| While of Expr * Statement
| Assign of string * Expr

At this point, we do not care about types: let's assume all expressions are correctly typed. Now consider the operational semantics of this language. Since the language supports variables, there must be some state s that maps variables to values. Let s be of type Variable \rightarrow \mathbb{Z} \cup \{ tt, ff \}. Each statement has the ability to mutate this state. It is possible to model the semantics of statements as some function sems \in Statement \rightarrow State \hookrightarrow State. Semantics of expressions can be modelled by a function seme \in Expr \rightarrow State \rightarrow \mathbb{Z} \cup \{ tt, ff \}. Note that the function produced by sems is partial since there is a while construct in our language, therefore allowing non-termination. Now let's go back to F# and define some more constructs:


type Result        = Int of int | Bool of bool
type State         = string -> Result
type Sem           = State  -> Result * State

The f# implementation is slightly different from the functions that we defined earlier. Statements also produce values (e.g. a return statement produces the value of an expression) and expressions can mutate state. Let us see how an implementation of sems looks like in F#:


let rec sems stmnt s = 
      match stmnt with
      | If(cond, tt, ff) ->
         let ((Bool b), s') = seme cond s
         if b then sems tt s' else (match ff with | Some(ff) -> sems ff s' | _ -> s')
      ... etc

In the above implementation, state is passed around very explicitly and results in many s's all over the place. It is possible to abstract from this and implicitly pass state around through the use of a few combinators:


let zero      = fun s -> (Int(0), s)
let ret x     = fun s -> (x, s) 
let (>>=) f g = fun s -> (fun (r, s') -> g r s') (f s)
let (>>|) f g = f >>= fun _ -> g

Note the types of the combinators in the context of semantics: ret \in Result \rightarrow Sem, (>>=) \in Sem \rightarrow (Result \rightarrow Sem) \rightarrow Sem and (>>|) \in Sem \rightarrow Sem \rightarrow Sem. Now we apply these combinators in the implementation of sems:


let rec sems stmnt = 
      match stmnt with
      | If(cond, tt, ff) ->
         seme cond 
         >>= fun ((Bool b)) -> if b then sems tt else (match ff with | Some(ff) -> sems ff | _ -> zero)
      ... etc

Ok, so the problem of explicit state passing is solved. Now we will look at the "... etc" part and fill in the semantics for other statements. Consider the semantics of the block statement: a sequence of statements S_0 to S_n is 'executed'. The state is mutated by each of these statements. If we forget about the result and only consider state, such a semantic will look like this:  sems \ [ S_0; S_1; \ ... \ S_n ] (s) \ = \ sems \ S_n \ (sems \ S_{n-1} \ ( \ ... \ sems \ S_1 \ ( \ sems \ S_0 \ s \ ) \ ... \ ) ) . We can utilize our >>| combinator to create such a chain: S_0 \ >>| \ S_1 \ >>| \ ... \ >>| \ S_n. In f#, we use the fold function. Each chain begins with 'zero' that has no effect on the state:


List.fold (fun chain S -> chain >>| sems S) zero slist

Now consider the semantics for the while statement: while some condition holds, execute the body. We can change this into the equivalent statement: if some condition holds, execute the body and execute the while statement again. Formally, this is defined like this: <\textrm{while} \ ( \ B \ ) \{ \ P \ \}, s> \rightarrow <\textrm{if} \ ( \ B  \ ) \{ \ P; \ \textrm{while} \ ( \ B \ ) \{ \ P \ \} \}, s>. In f#:


sems (While(B, P)) = sems (If(B, Block([P; While(B, P)]), None))

The semantic of the assign statement is remaining. State is a function that maps variables to values. The assign statement needs to mutate this state, but the problem is that a function cannot be mutated. Instead, we construct a new state that maps the variable to the new value. Formally, we define a function write \in State \times Var \times Result \rightarrow State with definition:

 write(s, var, val) = \lambda var' \in Var. \left\{  \begin{array}{l l} val & \quad \text{if var = var' }\\ s \ var' & \quad \text{otherwise}\\ \end{array} \right.

In f#, we can write this like:


let write var v = fun s -> (v, fun var' -> if var' = var then v else s var')
let read var    = fun s -> (s var, s)

Let's now fill in the blanks:


let intBinOp f (Int(l)) (Int(r)) = Int(f l r)

let binOpMap = 
            dict [
                    Plus,   intBinOp (+);
                    Subtr,  intBinOp (-);
                    Div,    intBinOp (/);
                    Mul,    intBinOp (*);
                    Eq,     fun (Int(l)) (Int(r)) -> Bool(l = r);
                    And,    fun (Bool(l)) (Bool(r)) -> Bool(l && r);
                 ]

let unOpMap =
            dict [
                    Not,    fun (Bool(n))           -> Bool(not n)
                 ]

let rec sems stmnt : Sem = 
      match stmnt with
      | If(cond, tt, ff) ->
         seme cond 
         >>= fun ((Bool b)) -> if b then sems tt else (match ff with | Some(ff) -> sems ff | _ -> zero)
      | While(B, P)      -> sems (If(B, Block([P; While(B, P)]), None))
      | Block(slist)     -> List.fold (fun chain S -> chain >>| sems S) zero slist
      | Assign(var, v)   -> seme v >>= write var

and seme expr : Sem = 
      match expr with
      | Expr.Int(n)   -> ret (Int(n))
      | Variable(v)   -> read v
      | Expr.Bool(b)  -> ret (Bool(b))
      | BinOp(op, l, r) ->
         let opf = binOpMap.[op]
         seme l 
         >>= fun l -> 
             seme r
             >>= fun r -> ret (opf l r)
      | UnOp(op, e) ->
         let opf = unOpMap.[op]
         seme e
         >>= fun e -> ret (opf e)