Few months ago, Cheryl birthday puzzle has has been an internet phenomenon. If you found the puzzle tricky to solve, we are in the same boat. However, if you observe, the puzzle only requires us to apply simple logic; not number theory or complex arithmetic, just simple logic. What, then, makes the puzzle tricky?

I attribute its trickiness to the chain of reasoning involved - repeated application of simple logic to the existing knowledge to make new deductions until we arrive at the solution. Since the reasoning is quite involved, it would be great if we can enlist the services of a computer to help us in the process. But, how can a computer assist us in making deductions? The answer lies in the well-known SAT problem.

## Knights and Knaves Puzzle

Consider the following simple instance of the famous Knights and Knaves class of puzzles:

```
There is an island in which certain inhabitants, called knights
always tell the truth, and others, called knaves always lie. It is
assumed that every inhabitant of this island is either a knight or
a knave.
Suppose A says, “Either I am a knave or B is a knight.”
What are A and B?
```

The puzzle is easy to solve mentally. Nonetheless, if you have a 2-SAT solver handy, you can also let solver do the work. Here is how:

Let `AisKnight`

and `BisKnight`

be boolean variables, denoting the
propositions “A is a Knight”, and “B is a Knight”, respectively. Since
an inhabitant can either be Knight or Knave but not both, boolean
formulas `¬ AisKnight`

and `¬ BisKnight`

denote the propositions that
“A is a Knave”, and “B is a Knave”, respectively.

Now, consider the statement made by A: “Either I am a knave or B is a
knight”. Symbolically, it is equivalent to: ```
(¬ AisKnight) ∨
BisKnight
```

. Since Knights always speak truth, and Knaves always lie,
the statement is true if A is a Knight, and false if A is a Knave. In
other words, the statement holds if and only if A is a Knight.
Symbolically, it means:

```
AisKnight ⇔ (¬ AisKnight) ∨ BisKnight
```

Observe that the above boolean formula *completely* describes the
constraints imposed by the puzzle, and does so quite succinctly. If
the above formula is satisfiable, then the constraints imposed by the
puzzle are also satisfiable, which means that puzzle has a solution.
Furthermore, the satisfying assignment to literals in the formula
(i.e., their truth values) give us the solution to the puzzle. To get
those satisfying assignments is what the 2-SAT solver is for. If we
feed the above formula to a 2-SAT solver, we get `AisKnight = true`

and
`BisKnight = true`

as satisfying assignments, telling us that A and B
are both knights.

Note that satisfying assignment only tells us that “if A is knight, then the puzzle is solved”. Maybe the puzzle is also solved if A is a knave. How do we check for this possibility? Again, using the solver. We explicitly encode the constraint that A is Knave, and ask if our constraints are satisfiable. The boolean formula is shown below:

```
(AisKnight ⇔ (¬ AisKnight) ∨ BisKnight) ∧ (¬ AisKnight)
```

A 2-SAT solver cannot find any satisfying assignment to the above formula, indicating that our constraints are unsatisfiable. Hence, A can never be a Knave.

Now, lets take a step back and summarize what we have done. We were given a puzzle that is not difficult, but not obvious either. Instead of doing the reasoning ourselves, we simply described the puzzle as a boolean formula, and let a SAT solver do the reasoning for us. In other words, we have outsourced the reasoning to a solver.This facility to outsource some or all of the reasoning to a solver can be quite handy when we are solving logical puzzles that require more complex reasoning, like Cheryl’s birthday puzzle.

## From SAT solvers to SMT solvers

Like the Knights and Knaves puzzle, most logical thinking puzzles can
be encoded as logical formulas, whose satisfiability determines the
solution of the puzzle. However, quite often puzzles are complex
enough that encoding them as boolean formulas in propositional logic
is cumbersome and impractical. This is akin to having to write every
program in assembly language. Often, we encounter situations where a
puzzle can be expressed as simple constraints in more complex
*theories*, like arithmetic, but translating the constraints into
propositional logic might seem impossible. An example is the 8-Queens
puzzle, where
constraints can be straightforwardly expressed using equalities and
inequalities in linear
arithmetic,
but doing the same using only boolean variables is quite complicated.

It turns out that are some complex theories, including linear
arithmetic, in which constraints expressed can *always* be translated
as constraints into propositional logic. More precisely, there exist
algorithms that can translate constraints expressed in these theories
into propositional logic without ever failing! This means that we can
describe puzzles as constraints in high-level theories like
arithmetic, which is relatively easy, then make use of these
algorithms to translate such constraints into boolean constraints, and
finally use a SAT solver to find satisfying assignments. Such
satisfying assignments can then be mapped back into original theory
(possibly arithmetic) to yield the solution to the puzzle. Wouldn’t it
be great if there is a tool that can do all of this?

Fortunately, such tools already exist; they are called SMT solvers. SMT is short for Satisfiability Modulo Theories, which informally means that it is a SAT solver extended with theories. Besides linear arithmetic, SMT solvers support various other theories, like BitVector arithmetic, sets, multi-sets, arrays, and to some extent quantification. There are many SMT solvers that are open source and freely available, but one that has proved its mettle in various industrial and research projects is Microsoft’s Z3 SMT solver [4].

Z3 has an easily-readable tutorial page that demonstrates how to use the tool to solve constraints in various theories. They even have a very cool web interface to make it easy for us to play around. SMT solvers, including Z3, have a standardized input language called SMT-LIB to describe constraints in any theory they support. As a simple example, here is the translation of boolean formula describing the Knights and Knaves puzzle in SMT-LIB language:

```
(declare-const AisKnight Bool)
(declare-const BisKnight Bool)
(assert (= AisKnight (or (not AisKnight) BisKnight)))
(check-sat)
(get-model)
```

The explanations for keywords like `declare-const`

and `assert`

are
found on the tutorial page. The
command `check-sat`

asks Z3 to check if the constraints stated so far
are satisfiable. It returns/prints either `sat`

or `unsat`

. The next
command `get-model`

asks Z3 to return/print the model if the formula
is satisfiable. A
model is simply a collection of satisfying assignments to unknowns in
the variables of the formula. For the above formula, any model should
contain `true`

as the satisfying assignment to both the variables
`AisKnight`

and `BisKnight`

denoting that A and B both are knights. I
have also made a permalink to Z3’s
web-interface containing the above code. If you visit the page and
click on the play button, you will see the model that Z3 constructed
for the formula. It should be similar to the following:

```
(model
(define-fun AisKnight () Bool
true)
(define-fun BisKnight () Bool
true)
)
```

Model describes `AisKnight`

and `BisKnight`

as nullary functions
instead of variables, but this is a mere technicality that you should
ignore.

When I first encoded the Knights and Knaves puzzle in Z3, my encoding is a little longer (and more closer to puzzle’s English description) than the one we have seen. Here is the SMT-LIB code:

```
(declare-const AisKnight Bool)
(declare-const AisKnave Bool)
(declare-const BisKnight Bool)
(declare-const BisKnave Bool)
;; A is either a Knight or a knave, but not both.
(assert (xor AisKnight AisKnave))
;; Likewise, B.
(assert (xor BisKnight BisKnave))
;; A's statement
(declare-const AStatement Bool)
(assert (= AStatement (or AisKnave BisKnight)))
;; If A is a Knight, then A's statement is true.
(assert (=> AisKnight AStatement))
;; If A is a Knave, then A's statement is a total lie
(assert (=> AisKnave (not AStatement)))
(check-sat)
(get-model)
```

You can also see it’s permanent page on Z3’s web interface.

## 8-Queens

I confess that Knights and Knaves is a pretty simple puzzle to warrant the fuss we have made. A more worthy candidate is 8-Queens puzzle. Fortunately, Nikolaj Bjørner, a co-creator of Z3, has written a succinct tutorial describing how to solve the more general n-Queens problem making use of BitVector theory in Z3. I encourage you to take a look.

## Cheryl Birthday Puzzle

We shall now see how formal logic and Z3 to can be used to simplify the reasoning required to solve Cheryl’s birthday puzzle. For the impatient, here is the solution.

First, let us recall the problem statement. Here is the text:

```
Albert and Bernard just became friends with Cheryl, and they want to
know when her birthday is.
Cheryl gave them a list of 10 possible dates:
May 15 May 16 May 19
June 17 June 18
July 14 July 16
August 14 August 15 August 17
Cheryl then tells Albert and Bernard separately the month and the day
of the birthday respectively.
Albert: I don't know when Cheryl's birthday is, but I know that
Bernard does not know too.
Bernard: At first I don't know when Cheryl's birthday is, but I know
now.
Albert: Then I also know when Cheryl's birthday is.
So when is Cheryl's birthday?
```

First of all, we need to model dates as the date type is not available
in Z3. Since Cheryl treats month and day of her birthday
independently, we need to model them independently, and then model
date as a combination of month and day. We don’t have to consider all
the months, or all the days; the ones in the possible dates are
enough. We model months as BitVectors of length 2 (i.e., two bits),
and days as BitVectors of length 3 respectively. There are two other
attractive alternatives to BitVectors: integers, and uninterpreted
sorts. Unlike BitVectors, which are finite, an integer in Z3 is an
unbounded datatype, hence makes reasoning unnecessarily difficult.
Declaring an uninterpreted sort (call it `T`

) in Z3 introduces a new
type `T`

, whose values have no attached interpretation, unlike, say,
integers. We could have introduced `Month`

as an uninterpreted sort,
and then declared `May`

etc as values of sort `Month`

. But this is not
enough; we must also explicitly assert that (a). No other value
besides declared values (i.e. `May`

, `June`

, `July`

, and `August`

)
have the sort `Month`

, and (b). None of the declared values is equal
to the other. Sans these constraints, Z3 is free to add more values
to the sort `Month`

, and can even assume that `May`

and `June`

are the
same.

Using BitVectors of length 2, here is how we model months:

```
;; define-sort is like typedef.
(define-sort M () (_ BitVec 2))
(declare-const may M)
(assert (= may #b00))
(declare-const june M)
(assert (= june #b01))
(declare-const july M)
(assert (= july #b10))
(declare-const aug M)
(assert (= aug #b11))
```

Similarly, days using BitVectors of length 3:

```
;; Days
(define-sort D () (_ BitVec 3))
(declare-const _14 D)
(assert (= _14 #b000))
(declare-const _15 D)
(assert (= _15 #b001))
(declare-const _16 D)
(assert (= _16 #b010))
(declare-const _17 D)
(assert (= _17 #b011))
(declare-const _18 D)
(assert (= _18 #b100))
(declare-const _19 D)
(assert (= _19 #b101))
```

You might have noticed that BitVectors of length 3 allow 8 values,
whereas we have only 6 possible days. BitVectors `#b110`

and `#b111`

do not correspond to valid days. Furthermore, not all combinations of
months and days are candidate dates for Cheryl’s birthday; only 10 of
them are valid. We therefore define an `isDate`

predicate (i.e., a
function whose co-domain is Bool) on months and days to define which
dates are valid dates:

```
;; What is a date?
(define-fun isDate ((m M)(d D)) Bool
(or (and (= m may) (or (= d _15) (= d _16) (= d _19)))
(and (= m june) (or (= d _17) (= d _18)))
(and (= m july) (or (= d _14) (= d _16)))
(and (= m aug) (or (= d _14) (= d _15) (= d _17)))))
```

Now that we have modeled months, days and dates, we have the
scaffolding ready to state the constraints of the puzzle. Firstly,
since we are interested in knowing actual month and day of Cheryl’s
birthday, we declare them as two unknowns - `bdaym`

and `bdayd`

of
month and day type respectively:

```
(declare-const bdaym M)
(declare-const bdayd D)
```

The idea is that, once we have described all the constraints of the
puzzle, satisfying assignments to `bdaym`

and `bdayd`

are the
BitVector representations of month and day of Chery’s actual birthday.

Now, lets consider the two propositions made by Albert in his first statement:

- Prop1: “I don’t know when Cheryl’s birthday is”.
- Prop2: “I know that Bernard does not know too”.

Let us represent the above two propositions as two boolean variables,
namely `aDoesntKnow`

and `aKnowsBDoesnt`

, respectively. Considering
that Albert does know `bdaym`

(Cheryl told him), the only way he
cannot know the birthday date is if `bdaym`

is a month with many days.
Let us say there is a predicate called `hasManyDays(m)`

that precisely
expresses the fact that a given month (`m`

) has many days. Then,
`aDoesntKnow`

is true if and only if `hasManyDays(bdaym)`

is true:

```
(assert (= aDoesntKnow (hasManyDays bdaym)))
```

Here is the definition of `hasManyDays(m)`

predicate:

```
(define-fun hasManyDays ((m M)) Bool
(exists ((d1 D) (d2 D))
(and (not (= d1 d2)) (isDate m d1) (isDate m d2))))
```

The definition simply says that a given month `m`

hasManyDays if and
only if there exist two days `d1`

and `d2`

such that `d1 ≠ d2`

, and
`isDate m d1`

is true and `isDate m d2`

is also true. In other words,
there exist two distinct days in the month `m`

.

Now, let us consider Prop2. Albert is aware that Bernard knows the day
of the birtday (`bdayd`

). Although Albert himself is not aware of
`bdayd`

, he knows that it must be a day occuring in `bdaym`

. Now, if
there exists a day (call it `d`

) in `bdaym`

that occurs uniquely in
`bdaym`

(i.e., `∀m. isDate (m,d) ⇒ m = bdaym`

), and `bdayd`

happens to
be that day, then Bernard can deduce the `bdaym`

from `bdayd`

, and can
consequently know Cheryl’s birthyday. However, Albert is sure that
this is not possible and Bernard does not know the birthday. This
means that no day occurs uniquely in `bdaym`

.

Let us say that there is a predicate `hasNoUniqueDay(m)`

that asserts
that the given month (`m`

) has no days that uniquely identify `m`

.
Then, Albert can be sure that Bernard does not know the birthday if
and only if `hasNoUniqueDay(bdaym)`

is true:

```
(assert (= aKnowsBDoesnt (hasNoUniqueDay bdaym)))
```

Here is the definition of `hasNoUniqueDay(m)`

predicate:

```
(define-fun hasNoUniqueDay ((m M)) Bool
(forall ((d D)) (=> (isDate m d)
(exists ((_m M)) (and (not (= _m m)) (isDate _m d))))))
```

The predicate simply states that the given month `m`

hasNoUniqueDay
if and only if all days `d`

in month `m`

also occur in alteast one
another month `_m`

.

We have now captured both the propositions made by Albert in his first statement as formulas. All that remains is to assert that the formulas are true:

```
(assert (and aDoesntKnow aKnowsBDoesnt))
```

Before we consider Bernard’s statement, let us take a step back and
make one crucial observation. We have modeled whatever Albert has
said, and it led to two constraints on `bdaym`

: `hasManyDays(bdaym)`

is true and `hasNoUniqueDay(bdaym)`

is true. Therefore, due to the
statements made by Albert, we know have information about `bdaym`

,
namely that it has many days and that it has no day that uniquely
identifies it. Since Bernard listened to Albert, he would also have
deduced the same.

Now, lets consider propositions made by Bernard in his only statement:

- Prop3: At first I don’t know when Cheryl’s birthday is.
- Prop4: I now know when Chery’s birthday is.

Prop3 is simply a reaffirmation of Albert’s Prop2. Prop4, however, is
very important. It effectively says that whatever Albert has said
about `bdaym`

coupled with the knowledge of `bdayd`

is enough to
deduce the birthday. In other words, any month (`m`

) containing
`bdayd`

and satisfying Albert’s constraints (viz., `hasManyDays(m)`

and `hasNoUniqueDay(m)`

) must be unique, and it has to be `bdaym`

.
More precisely:

```
(assert (forall ((m M))
(=> (and (hasManyDays m) (hasNoUniqueDay m)
(isDate m bdayd))
(= m bdaym))))
```

For convenience, we factor the above constraint into a predicate
called `determinesBdayM`

on any day `d`

, and use it to constraint
`bdayd`

:

```
(define-fun determinesBdayM ((d D)) Bool
(forall ((m M))
(=> (and (hasManyDays m) (hasNoUniqueDay m)
(isDate m d))
(= m bdaym))))
(assert (determinesBdayM bdayd))
```

Before we consider Albert’s final statement, we make another important
observation. We have captured whatever Bernard has said about the
`bdayd`

, and it gave us one constraint on `bdayd`

, namely that
`determinesBdayM(bdayd)`

is true. Albert too would have made this
deduction.

In his final statement, Albert declares that he too knows the birthday
now. Since Albert already knows the birthday month (`bdaym`

), this
means that any day (`d`

) in `bdaym`

that satisfies Bernard’s
constraints must be unique, and it must be `bdayd`

. More precisely:

```
(assert (forall ((d D))
(=> (and (isDate bdaym d) (determinesBdayM d))
(= d bdayd))))
```

Thats it. We have no more constraints to capture. Using Z3, we now
check if the given constraints are satisfiable, and if they are, then
ask it to return a satisfying assignment. To do this, go to this
page containing all the SMT-LIB
statements we have made so far, and then click on the play button. Z3
should print sat, followed by a long model describing satisfying
assignment to every variable in our long formula. Since we are only
interested in knowing `bdaym`

and `bdayd`

, we only pay attention to
relevant parts in the model:

```
(define-fun bdaym () (_ BitVec 2)
#b10)
(define-fun bdayd () (_ BitVec 3)
#b010)
```

Among months, `#b10`

stands for July, and among days `#b010`

stands
for 16th. Therefore, Z3’s solution to Cheryl’s birthday problem is
July 16th, which happens to be the actual answer!

## Final Remarks

This blog should have hopefully demonstrated the utility of including a SAT/SMT solver in the workflow when the problem demands us to make a sequence of nontrivial logical deductions. If you are new to formal reasoning tools, like SMT solvers, you may have many questions including:

- Does the ability to do away with some amount of manual reasoning worth the substantial effort required to describe everything in formal logic?, and
- Why can’t we simply write some code to solve the puzzle instead of encoding it rigorously in logic?

The answer to both the questions is the same: the benefits of formally
modeling a problem in an automatic reasoning tool goes beyond its end
product, i.e., the solution to the problem. Formal modeling is also a
medium that (a). enables us to think precisely about the problem, and
(b). lets us understand *what* should be the solution to the problem,
without necessarily requiring us to think about *how* to construct it
(unlike writing code). In other words, formal modeling drastically
improves our thinking and makes us better problem solvers. To quote
Leslie Lamport: “Writing is nature’s way of letting you know how
sloppy your thinking is, mathematics is nature’s way of letting you
know how sloppy your writing is, and Formal mathematics is nature’s
way of letting you know how sloppy your mathematics is.”

In this blog, I have used puzzle solving as a vehicle for
demonstrating the ability of SMT solvers in assisting with our
thought process. However, the utility of solvers extends well beyond
puzzle solving. Today, they power some of the state-of-the-art program
analysis and verification tools that perform heavyweight reasoning on
computer programs to automatically find bugs, and sometimes to even
prove that a certain class of bugs (e.g. null pointer dereferences, or
`ArrayOutOfBounds`

) do not exist in the program. If you are interested
in finding out some more cool tricks possible via SMT solvers, I
encourage you to take a look at Torlak et al’s Onward’13 and PLDI’14
papers describing their Rosette solver-aided language.