# Lab 5: SAT Solver solution

\$24.99

Original Work
Category:

## Description

5/5 - (1 vote)

rule1 = adamC or adamH or chris or duane 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 adamC or not adamH) and (not adamC or not chris) \ and (not adamC or not duane) and (not adamC or not tim) \ and (not adamH or not chris) and (not adamH or not duane) \ and (not adamH or not tim) and (not chris or not duane) \ and (not chris or not tim) and (not duane or not tim) # Only one of the suspects is guilty. In other words, for any pair of suspects, # at least one must be NOT guilty. That means we can’t find a pair of guilty # suspects.
rule3 = (not chocolate or not vanilla or not pickles) \ and (chocolate or vanilla) and (chocolate or pickles) and (vanilla or pickles) # It can’t be that all flavors were present, and among any pair of flavors, at # least one was present.
rule4 = (not adamC or pickles) and (not adamC or not chocolate) \ and (not adamC or not vanilla) # If Adam C. is not guilty, this will be true. Otherwise, it will be true if # only pickles-flavored cupcakes were present.
rule5 = (not chris or duane) and (not duane or chris) # If Chris ate cupcakes without sharing with Duane, the first case will fail to # hold. Likewise for Duane eating without sharing.
rule6 = (not adamH or chocolate) and (not adamH or vanilla) \ and (not adamH or pickles) # If Adam H. is the culprit and we left out a flavor, the corresponding case # here will fail to hold.
rules = rule1 and rule2 and rule3 and rule4 and rule5 and rule6
For some practice coming up with Boolean formulas, consider this truth table, explaining which values of Boolean variables a , b , and c lead to which values of a formula. We write T for True and F for False . abcAnswer FFFF TFFF FTFF TTFF FFTF TFTF FTTF TTTT Write a Python formula over a , b , and c that matches the truth table. (The format should be as in the puzzle encoding above, e.g. adam or not (chris and duane) , and your formula need not follow the “CNF” restriction introduced below).
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) (https://en.wikipedia.org/wiki/Conjunctive_normal_form). We say that a literal is a variable or the not of a
variable. Then a clause is a multi-way or of literals, and a CNF formula is a multi-way and of clauses. When we commit to this restrictive format, we can represent: a variable as a Python string a literal as a pair of a variable and a Boolean value ( False if not 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.
Consider this Boolean formula.
(c or b) and a and a and not a and (c or a)
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.
((b or c) and not a) or (a and b and (a or c))
Write an equivalent CNF formula (as a Python literal), in the format used in the lab (e.g., [[(‘a’, True), (‘b’, False)], [(‘c’, True)]] ).
A classic tool that works on Boolean formulas is a satisfiability solver (https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Algorithms_for_solving_SAT), 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:
satisfying_assignment(rules) {‘duane’: False, ‘chris’: False, ‘chocolate’: False, ‘adamH’: False, ‘adamC’: 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. So, we see that Tim the Beaver is guilty and has a taste for vanilla and pickles! Actually, other legal answers would have had Tim enjoying other flavors, too. However, 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.
satisfying_assignment(rules + [[(‘tim’, False)]]) # Nothing printed (corresponds to answer of None)
There’s one very easy 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 length-N sequences of Booleans.
def all_bools_generator(length): if length == 0: yield [] else: for v in all_bools_generator(length-1): 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!
(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. For completeness, here is how we update the formula when we learn c = False .
d
Note that, with this formula, it is rather obvious which variable to set next and what Boolean value to give it! That brings us to the next topic (after an interlude of two questions to check your understanding). Consider this CNF formula.
(c or c or b) and (not a or b or not c)
Write a CNF formula (in normal Python expression syntax, e.g. (a or b) and (c or not d) ) for the case where a = True , without using variable a . Write None if this assignment falsifies the formula, and leave the blank empty if this assignment renders the formula true.
Write a CNF formula (in normal Python expression syntax, e.g. (a or b) and (c or not d) ) for the case where a = False , without using variable a . Write None if this assignment falsifies the formula, and leave the blank empty if this assignment renders the formula true.
A further optimization to this procedure will be needed, to pass all of the test cases quickly enough. The one we require you to implement is unit propagation, a heuristic for choosing variables to split on. Namely, at the start of any call to your procedure, check if the formula contains any length-one clauses. If such a clause [(x, b)] exists, then we may set x to Boolean value b , just as we do in the True and False cases of the outline above. However, we know that, if this setting leads to failure, there is no need to backtrack and also try x = not b ! The reason is that the unit clause alone tells us exactly what the value of x must be. So, for your unit-propagation optimization, begin the function with a loop that repeatedly finds unit clauses, if any, and propagates their consequences through the formula. One unit propagation 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 first half of our test cases in time. 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).
4) Scheduling by Reduction 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 formulas are 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 simple scheduling problem. In particular, we are interested in the real-life problem of assigning 6.009 students to different sessions for taking a quiz. Each student is available for only some of the sessions, but each session has limited capacity. We want to find a schedule (assignment of students to sessions) that respects all the constraints. Please implement function boolify_scheduling_problem(student_preferences, session_capacities) . Argument student_preferences is a dictionary mapping a student name (string) to a set of session names (strings) when that student is available. Argument session_capacities is a dictionary mapping each session name to a positive integer for how many students can fit in that session. 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’, ‘penthouse’}}, {‘basement’: 1, ‘kitchen’: 2, ‘penthouse’: 3})
In English, Alice is available for the sessions in the basement and penthouse, and Bob is available for the sessions in the kitchen and penthouse. The basement can fit 1 student, the kitchen 2 students, and the penthouse 3 students. One legal schedule would be Alice in the basement and Bob in the kitchen. 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_session , where student is the name of a student, and where session is the name of a session. (We will only call your code on student and session names that are free of underscore characters, so there is no issue with ambiguity in naming Boolean variables.) The variable student_session should be True if and only if that student is assigned to that session. The CNF clauses you include should enforce exactly the following rules: 1. Each student is assigned to exactly one session. 2. Students are only assigned to sessions included in their preferences. 3. No session 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 “dumb” translation to CNF formulas. One concrete manifestation of that rule is that your translation should consider students and sessions completely separately, effectively generating a separate CNF formula for each and combining them with and . The formula for some student preferences should be usable accurately with the formula for any session capacities (though the latter depends on the names of available students, but not their preferences). During 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 directly encode answers.
\ / /\__/\ \__=( o_O )= (__________) |_ |_ |_ |_