Lab 6: SAT Solver
If you are a current student, please Log In for full access to the web site.
Note that this link will take you to an external site (https://shimmer.mit.edu) to authenticate, and then you will be redirected back to this page.
Table of Contents
 1) Preparation
 2) Introduction
 3) SAT Solver
 4) Implementation
 5) Scheduling by Reduction
 6) UI
 7) Code Submission
 8) Checkoff
1) Preparation§
This lab assumes you have Python 3.6 or later installed on your machine (3.9 recommended).
The following file contains code and other resources as a starting point for this lab: lab6.zip
Most of your changes should be made to lab.py
, which you will submit at the
end of this lab. Importantly, you should not add any imports to the file.
You can also see and participate in online discussion about this lab in the "Lab 6" Category in the forum.
This lab is worth a total of 4 points. Your score for the lab is based on:
 answering the questions on this page (0.5 points)
 passing the test cases from
test.py
under the time limit (2 points), and  a brief "checkoff" conversation with a staff member to discuss your code (1.5 points).
Note that passing all of the tests on the server will require that your code runs reasonably efficiently.
Please also review the collaboration policy before continuing.
The questions in sections 13 (inclusive) are due before lecture, at 11:00am Eastern on Monday, 5 April. The other questions on this page (including your code submission) are due at 5pm Eastern on Friday, 9 April. The checkoff is due at 10pm Eastern on Wednesday, 14 April.
2) Introduction§
From recreational mathematics to standardized tests, one popular problem genre is logic puzzles, where some space of possible choices is described using a list of rules. A solution to the puzzle is a choice (often the one unique choice) that obeys the rules. This lab should give you the tools to make short work of any of those puzzles, assuming you have your trusty Python interpreter.
Here's an example of the kind of logic puzzle we have in mind.
 The suspects are Saman, Manya, Jonathan, Max, and Tim the Beaver.
 Whichever suspect ate any of the cupcakes must have eaten all of them.
 The cupcakes included exactly two of the flavors chocolate, vanilla, and pickles.
 Saman only eats picklesflavored cupcakes.
 Years ago, Jonathan and Max made a pact that, whenever either of them eats cupcakes, they must share with the other one.
 Manya feels strongly about flavor fairness and will only eat cupcakes if she can include at least 3 different flavors.
Let's translate the problem into Boolean logic,
where we have a set of variables, each of which takes the value True
or False
.
We write the rules as conditions over these variables. Here is each rule as a
Python expression over Boolean variables. We include one variable for the
guilt of each suspect, plus one variable for each potential flavor of cupcake.
In reading these rules, note that Python not
binds more tightly than or
, so
that not p or q
is the same as (not p) or q
. It's also fine not to follow
every last detail, as this rule set is just presented as one example of a
general idea!
You may also find that some of our encoding choices don't match what you would come up with, such that our choices lead to longer or lesscomprehensible rules. We are actually intentionally forcing ourselves to adhere to a restricted format that we will explain shortly, and that will ultimately make the job of solving these kinds of problems more straightforward.
rule1 = (saman or manya or jonathan or max_ or tim)
# At least one of them must have committed the crime! Here, one of these
# variables being True represents that person having committed the crime.
rule2 = ((not saman or not manya)
and (not saman or not jonathan)
and (not saman or not max_)
and (not saman or not tim)
and (not manya or not jonathan)
and (not manya or not max_)
and (not manya or not tim)
and (not jonathan or not max_)
and (not jonathan or not tim)
and (not max_ or not tim))
# At most one of the suspects is guilty. In other words, for any pair of
# suspects, at least one must be NOT guilty (so that we cannot possibly find
# two or more people guilty).
# Together, rule2 and rule1 guarantee that exactly one suspect is guilty.
rule3 = ((not chocolate or not vanilla or not pickles)
and (chocolate or vanilla)
and (chocolate or pickles)
and (vanilla or pickles))
# Here is our rule that the cupcakes included exactly two of the flavors. Put
# another way: we can't have all flavors present; and, additionally, and among
# any pair of flavors, at least one was present.
rule4 = ((not saman or pickles)
and (not saman or not chocolate)
and (not saman or not vanilla))
# If Saman is guilty, this will evaluate to True only if only picklesflavored
# cupcakes were present. If Saman is not guilty, this will always evaluate to
# True. This is our way of encoding the fact that, if Saman is guilty, only
# picklesflavored cupcakes must have been present.
rule5 = (not jonathan or max_) and (not max_ or jonathan)
# If Jonathan ate cupcakes without sharing with Max, the first case will fail
# to hold. Likewise for Max eating without sharing. Since Jonathan and Max
# only eat cupcakes together, this rule excludes the possibility that only one
# of them ate cupcakes.
rule6 = ((not manya or chocolate)
and (not manya or vanilla)
and (not manya or pickles))
# If Manya is the culprit and we left out a flavor, the corresponding case here
# will fail to hold. So this rule encodes the restriction that Manya can only
# be guilty if all three types of cupcakes are present.
satisfied = rule1 and rule2 and rule3 and rule4 and rule5 and rule6
The piece of code above is a Python program that will tell us whether a given assignment is consistent with the rules we have laid out. For example, if we had set the following variables (representing the hypothesis that Saman was guilty and that only Picklesflavored cupcakes were present):
saman = True
manya = False
jonathan = False
max_ = False
tim = False
pickles = True
vanilla = False
chocolate = False
and then run the code, the satisfied
variable would be set to False
(since
rule3
would be False
), indicating that this assignment did not satisfy the
rules we had set out.
While code like the above could be useful in certain situations, it doesn't help us solve the problem (it only helps us check a possible solution). In this lab, we'll look at the problem of Boolean Satisfiability: our goal will be, given a description of Boolean variables and constraints on them (like that given above), to find a set of assignments that satisfies all of the given constraints.
2.1) Conjunctive Normal Form§
In encoding the puzzle, we followed a very regular structure in our Boolean formulas, one important enough to have a common name: conjunctive normal form (CNF).
In this form, we say that a literal is a variable or the not
of a variable.
Then a clause is a multiway or
of literals, and a CNF formula is a multiway and
of clauses.
It's okay if this representation does not feel completely natural. Some people find this form to be "backwards" from the way they would otherwise think about these constraints. However, forcing our constraints to be in this form can simplify the problem of implementing our solver, compared to other representations we could choose. We'll try in this writeup to help you with the pieces of the lab involving converting expressions to CNF.
2.1.1) Python Representation§
When we commit to representing problems in CNF, we can represent:
 a variable as a Python string
 a literal as a pair (a tuple), containing a variable and a Boolean value (
False
ifnot
appears in this literal,True
otherwise)  a clause as a list of literals
 a formula as a list of clauses
For example, our puzzle from above can be encoded as follows, where again it is OK not to read through every last detail.
rule1 = [[('saman', True), ('manya', True), ('jonathan', True),
('max', True), ('tim', True)]]
rule2 = [[('saman', False), ('manya', False)],
[('saman', False), ('jonathan', False)],
[('saman', False), ('max', False)],
[('saman', False), ('tim', False)],
[('manya', False), ('jonathan', False)],
[('manya', False), ('max', False)],
[('manya', False), ('tim', False)],
[('jonathan', False), ('max', False)],
[('jonathan', False), ('tim', False)],
[('max', False), ('tim', False)]]
rule3 = [[('chocolate', False), ('vanilla', False), ('pickles', False)],
[('chocolate', True), ('vanilla', True)],
[('chocolate', True), ('pickles', True)],
[('vanilla', True), ('pickles', True)]]
rule4 = [[('saman', False), ('pickles', True)],
[('saman', False), ('chocolate', False)],
[('saman', False), ('vanilla', False)]]
rule5 = [[('jonathan', False), ('max', True)],
[('max', False), ('jonathan', True)]]
rule6 = [[('manya', False), ('chocolate', True)],
[('manya', False), ('vanilla', True)],
[('manya', False), ('pickles', True)]]
rules = rule1 + rule2 + rule3 + rule4 + rule5 + rule6
When we have formulated things in this way, the list rules
contains a formula
that encodes all of the constraints we need to satisfy.
2.1.2) Examples§
c and (a or d) and (not b or a) and (not a or e or not d)
Write an equivalent CNF formula (as a Python literal), in the format used in the lab (e.g., [[('a', True), ('b', False)], [('c', True)]]
).
Now, consider this Boolean formula (which is not in CNF).
(a and b) or (c and not d)
This expression looks innocuous, but translating it into CNF is actually a nontrivial exercise! It turns out, though, that this expression does have a representation in CNF as:
(a or c) and (a or not d) and (b or c) and (b or not d)
or, in our representation, as:
[[('a', True), ('c', True)], [('a', True), ('d', False)], [('b', True), ('c', True)], [('b', True), ('d', False)]]
Notice that the above expression will be true if a
and b
are both true, or
if c
is true and d
is false.
a and (not b or (c and d))
Write an equivalent CNF formula (as a Python literal), in the format used in the lab (e.g., [[('a', True), ('b', False)], [('c', True)]]
).
3) SAT Solver§
A classic tool that works on Boolean formulas is a satisfiability solver or SAT solver. Given a formula, either the solver finds Boolean variable values that make the formula true, or the solver indicates that no solution exists. In this lab, you will write a SAT solver that can solve puzzles like ours, as in:
>>> print(satisfying_assignment(rules))
{'max': False, 'jonathan': False, 'chocolate': False, 'manya': False,
'saman': False, 'pickles': True, 'tim': True, 'vanilla': True}
The return value of satisfying_assignment
is a dictionary mapping variables
to the Boolean values that have been inferred for them (or None
if no valid
mapping exists).
So, we can see that, in our example above, Tim the Beaver is guilty and has a taste for vanilla and pickles!
It turns out that there are other possible answers that have Tim enjoying other flavors, but it also turns out that Tim is the uniquely determined culprit. How do we know? The SAT solver fails to find an assignment when we add an additional rule proclaiming Tim's innocence.
>>> print(satisfying_assignment(rules + [[('tim', False)]]))
None
3.1) The Naive Approach§
There's one straightforward, bruteforce way to solve Boolean puzzles: enumerate all possible Boolean assignments to the variables. Evaluate the rules on each assignment, returning the first assignment that works. Unfortunately, this process can take prohibitively long to run! For a concrete illustration of why, consider this Python code to generate all sequences of Booleans of a certain length.
When we have N Boolean variables in our puzzle, the possible assignments can be represented as lengthN sequences of Booleans.
def all_bools_generator(length):
if length == 0:
yield []
else:
for v in all_bools_generator(length1):
yield [True] + v
yield [False] + v
def all_bools(length):
return list(all_bools_generator(length))
Here's an example output.
>>> all_bools(3)
[[True, True, True], [False, True, True], [True, False, True],
[False, False, True], [True, True, False], [False, True, False],
[True, False, False], [False, False, False]]
We could get more ambitious and try to generate longer sequences.
>>> len(all_bools(3))
8
>>> len(all_bools(4))
16
>>> len(all_bools(5))
32
>>> len(all_bools(6))
64
>>> len(all_bools(20))
1048576
>>> len(all_bools(25))
# Python runs for long enough that we give up!
It's actually quite expensive even to run through all Boolean sequences of nontrivial lengths, let alone to test each sequence against the rules. The reason is that there are 2^N lengthN Boolean sequences, and that kind of exponential function grows quite quickly as the length N of our mappings grows.
Lots of logic puzzles can lead to hundreds of Boolean variables. Are we out of luck if we want Python to do all the work? Worry not! In this lab, you will implement a SAT solver that uses a much smarter algorithm than this bruteforce enumeration of all assignments, thanks to the magic of backtracking search.
3.2) A Nicer Approach§
Instead of enumerating all assignments, we will ask you to implement a more clever approach for Boolean satisfiability. One such approach is outlined below (with some of the details intentionally omitted):
We start by picking an arbitrary variable x from our formula F. We then
construct a related formula F_1, which does not involve x but incorporates
all the consequences of setting x to be True
. We then try to solve F_1.
If it produces a successful result, we can combine that result with information
about x being True
to produce our answer to the original problem.
If we could not solve F_1, we should try setting x to be False
instead.
If no solution exists in either of the above cases, then the formula F cannot
be satisfied.
3.2.1) Updating Expressions§
A key operation here is updating a formula to model the effect of a variable assignment. As an example, consider this starting formula.
(a or b or not c) and (c or d)
If we learn c = True
, then the formula should be updated as follows.
(a or b)
We removed not c
from the first clause, because we now know conclusively that
that literal is False
. Conversely, we can remove the second clause, because
with c
true, it is assured that the clause will be satisfied.
Note a key effect of this operation: variable d
has disappeared from the
formula, so we no longer need to consider values for d
.
In general, this approach often saves us from an exponential enumeration of variable values, because we learn that, in some branches of the search space, some variables are actually irrelevant to the problem.
This pruning will show up in the assignments that your SAT solver returns: you are allowed (but not required) to omit variables that turn out to be irrelevant.
If we had instead learned that c
was False
, we would update the formula
instead as follows:
d
How did we get there? Note that, with c
being False
, the first clause is
already satisfied. The second clause, though, will only be True
if d
is
True
.
It might be a good idea to implement this process (updating a formula based on a new assignment) as a helper function (which you can test independently), as we will need to perform this operation repeatedly.
3.2.2) Examples§
Consider this CNF formula, in the form we use in this lab:
[
[('a', True), ('b', True), ('c', True)],
[('a', False), ('f', True)],
[('d', False), ('e', True), ('a', True), ('g', True)],
[('h', False), ('c', True), ('a', False), ('f', True)],
]
a = True
, without using variable a
. Write the string 'falsifies'
if this assignment falsifies the formula, and write the string 'truthifies'
if this assignment renders the formula true.
a = False
, without using variable a
. Write the string 'falsifies'
if this assignment falsifies the formula, and write the string 'truthifies'
if this assignment renders the formula true.
a = True
and f = True
, without using variables a
or f
. Write the string 'falsifies'
if this assignment falsifies the formula, and write the string 'truthifies'
if this assignment renders the formula true.
a = True
and f = False
, without using variables a
or f
. Write the string 'falsifies'
if this assignment falsifies the formula, and write the string 'truthifies'
if this assignment renders the formula true.4) Implementation§
Implement the function satisfying_assignment
as described in lab.py
. Your
function should take as input a CNF formula (in the form described throughout
this writeup). It should return a dictionary mapping variable names to Boolean
values if there exists such an assignment that satisfies the given formula. If
no such assignment exists, it should return None
.
4.1) Optimizations§
A couple of further optimizations are likely to be necessary in order to pass all of the test cases quickly enough on the server:

In the procedure described above, if setting the value of x immediately leads to a contradiction, we can immediately discard that possibility (rather than waiting for a later step in the recursive process to notice the contradiction).

At the start of any call to your procedure, check if the formula contains any lengthone clauses ("unit" clauses). If such a clause
[(x, b)]
exists, then we may setx
to Boolean valueb
, just as we do in theTrue
andFalse
cases of the outline above. However, we know that, if this setting leads to failure, there is no need to backtrack and also tryx = not b
(because the unit clause alone tells us exactly what the value ofx
must be)!Thus, you can begin your function with a loop that repeatedly finds unit clauses, if any, and propagates their consequences through the formula. Propagating the effects of one unit clause may reveal further unit clauses, whose later propagations may themselves reveal more unit clauses, and so on.
Implementing function satisfying_assignment
in this way should allow your
code to pass the test_sat
and test_sat_sudoku
test cases in time. The
test_sat_sudoku
tests will use your SAT solver to solve sudoku puzzles,
which can also be expressed in CNF^{1}! These test cases are large, so consider
making smaller test cases to debug them.
You are free to add additional optimizations beyond what we laid out above, or even make broader changes to the algorithm, so long as you avoid "hard coding" for rather specific SAT problems (except for base cases like empty formulas).
5) Scheduling by Reduction§
Now that we have a fancy new SAT solver, let's look at applying it to a new problem!
In general, it's possible to write a new implementation of backtracking search for each new problem we encounter, but another strategy is to reduce a new problem to one that we already know how to solve well. Boolean satisfiability is a popular target for reductions, because a lot of effort has gone into building fast SAT solvers. In this last part of the lab, you will implement a reduction to SAT from a scheduling problem.
In particular, we are interested in the reallife problem of assigning 6.009 students to different rooms for taking a quiz (when 6.009 runs inperson, students take the quiz at the same time but in different rooms).
Each student is prefers only some of the rooms, but each room has limited capacity. We want to find a schedule (assignment of students to rooms) that respects all the constraints.
Please implement the function
boolify_scheduling_problem(student_preferences, room_capacities)
as described both below and in lab.py
:

The argument
student_preferences
is a dictionary mapping a student name (string) to a set of room names (strings) for which that student is available. 
Argument
room_capacities
is a dictionary mapping each room name to a positive integer for how many students can fit in that room. 
The function returns a CNF formula encoding the schedule problem, as we explain next.
Here's an example call:
boolify_scheduling_problem({'Alice': {'basement', 'penthouse'},
'Bob': {'kitchen'},
'Charles': {'basement', 'kitchen'},
'Dana': {'kitchen', 'penthouse', 'basement'}},
{'basement': 1,
'kitchen': 2,
'penthouse': 4})
In English, Alice is available for the sessions in the basement and penthouse, Bob is available only for the session in the kitchen, etc. The basement can fit 1 student, the kitchen 2 students, and the penthouse 4 students. In this case, one legal schedule would be Alice in the basement, Bob in the kitchen, Charles in the kitchen, and Dana in the penthouse.
Your job is to translate such inputs into CNF formulas, such that your SAT solver can then find a legal schedule (or confirm that none exists).
The CNF formula you output should mention only Boolean variables named like
student_room
, where student
is the name of a student, and where
room
is the name of a room.
The variable student_room
should be True
if and only if that student is
assigned to that room (for example, the variable Bob_kitchen
should be
True
if Bob is in the kitchen and False
otherwise).
The CNF clauses you include should enforce exactly the following rules (which are discussed in more detail below):
 Students are only assigned to rooms included in their preferences.
 Each student is assigned to exactly one room.
 No room has more assigned students than it can fit.
Our requirement for this part of the lab is that your code should not solve
the optimization problem. Rather, you should implement a translation to CNF
formulas (which satisfying_assignment
can then solve).
During the checkoff, our staff will try to make sure you've followed this rule and not merely, say, implemented a backtracking search directly for the scheduling problem, to output trivial CNF problems that encode answers directly.
5.1) Encoding the Rules§
Turning these rules into CNF formulas is a tricky task. We'll try to provide some guidance for thinking about each of these rules in the following sections (though if you get stuck, please don't hesitate to ask via the Forum).
Note that each of these rules can be expressed as its own CNF formula, and the
AND of these three rules represents the overall formula we need to solve. As
such, you may wish to write a helper function to generate the formula for each
of these rules and to use those helper functions in boolify_scheduling_problem
.
The examples below also make nice test cases to add to your lab.py or test.py (simpler than many we will test your code on)! Note also that computing the results for the examples below may also be difficult to do without some additional scratch paper (or at least a bigger text editing area than the little boxes below).
5.1.1) Students Only In Desired Sessions§
For each student, we need to guarantee that they are given a room that they selected as one of their preferences. In the example above, for example, we know that Charles must be in the basement or the kitchen, and that Alice must be in the basement or in the penthouse.
'Bob_kitchen'
represents Bob being in the
kitchen).How could you generate this formula from the arguments given to
boolify_scheduling_problem
?
5.1.2) Each Student In Exactly One Session§
This rule is a little bit trickier, but it may help to separate it into two pieces:
 each student must be in at least one room, and
 each student must be in at most one room.
We can generate formulae for each of these conditions and combine them to construct the overall formula corresponding to this rule.
In fact, the first bullet (that each student be assigned to at least one room) is redundant with our first condition (that each student be assigned to a room in their preferences).
So let's turn our attention to making sure that each student is assigned to at most one room. This one is a bit trickier, particularly since we need to put things in CNF. One flip of perspective that can be helpful is that, if we need each student to be in at most one room, that means that for any pair of rooms, any given student can be in only one of them.
For example, one clause in this expression will say that Bob cannot be in both
the kitchen and the basement. That is, we cannot have both Bob_kitchen
and
Bob_basement
be True
(or, to phrase it a different way, at least one of
them must be False
).
Note that there is a corresponding clause for every other pair of rooms; and each of these clauses has a corresponding clause for Alice (and the other students). For purposes of this question, include all rooms for each student, regardless of their preferences.
'Bob_kitchen'
represents Bob being in the kitchen).How could you generate this formula from the arguments given to
boolify_scheduling_problem
?
5.1.3) No Oversubscribed Sessions§
This last rule is also fairly tricky, and it maybe requires a bit of a shift of perspective to express this constraint in CNF. However, it is similar to the previous rule in some ways.
We can think about this as: if a given room can contain N students, then in every possible group of N+1 students, there must be at least one student who is not in the given room.
For example, since the kitchen holds 2 people, we would need to consider all possible groups of 3 students and make sure that at least one of the students in each group is not in that room. For purposes of this question, include all groups of students, regardless of their preferences.
What about the penthouse? It has enough room for everyone, so there is no need even to include it in the constraints (it doesn't constrain our decision in any way)!
'Bob_kitchen'
represents Bob being in the kitchen).How could you generate this formula from the arguments given to
boolify_scheduling_problem
?
6) UI§
We have provided a browser UI for this lab, so you can see your code solving
scheduling problems in action! When you have implemented both main functions
of the lab, you may run python3 server.py
and navigate to http://localhost:6009/
. Running a test case on the UI
involves generating a CNF formula and searching for a satisfying assignment for
it, done by calling your functions. Enjoy!
7) Code Submission§
Once you have debugged your code locally and are satisfied, upload your
lab.py
below:
8) Checkoff§
Once you are finished with the code, please come to office hours and add yourself to the queue asking for a checkoff. You must be ready to discuss your code and test cases in detail before asking for a checkoff.
You should be prepared to demonstrate your code (which should be wellcommented, should avoid repetition, and should make good use of helper functions). In particular, be prepared to discuss:
 In English, the general recipe for finding assignments that satisfy a given CNF formula.
 In English, your strategy for updating a formula based on setting an variable to be
True
orFalse
.  Your implementation of
satisfying_assignment
, including any helper functions.  In English, the general recipe you came up with for translating scheduling problems into CNF formulas (including all three rules).
 Your code for
boolify_scheduling_problem
to implement that recipe.
8.1) Grade§
Footnotes
^{1}For a brief description of how these test cases were generated, see this link, which describes the process.