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 = trueand
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.