Satisfiability and SAT solvers
We review the notion of satisfiability and SAT formula via an example. Also pointers to SAT solvers are provided.
Satisfiability
Satisfiability problem
Recall that the Satisfiability problem is to decide, given a SAT formula (we will assume it is in CNF ), whether it is satisfiable (or consistent) or not. Sometimes, if the CNF SAT formula is satisfiable/consistent, we would also like to compute a satisfying assignment (or model).
If you need a refresher, the following short video might be useful:
SAT Solvers
A SAT solver is a tool that takes as input a CNF formula and outputs either a satisfying Boolean assignment to the variables used in the CNF formula if the formula is consistent or UNSAT if it is not.
These solvers are typically binaries which accept input in the form of a text file with the CNF formula and write the relevant output to the console.
If you are interested, Lingeling is the exact SAT solver we are using to grade your submission. Instructions for installation are in the README. Note that we will not be able to provide any support for local execution and testing, please use the SAT Solver submission on Autolab created specifically for this purpose to test your generated SAT formulas out.
Representing SAT formulas in Lingeling
While the standard theoretical notation for a SAT formula is the CNF with propositional logic, in this section we will consider an alternate format to represent CNF SAT formulas that is employed by SAT solvers. We will present this format via an example, where we first present things in propositional logic and then present its corresponding representation for SAT solvers.
Consider the following data provided to you regarding course codes and their corresponding prerequisites. The data is in the form <course code> [<identifier>]: <prerequisites> (if any)
CSE115 [1]: No prerequisites
CSE116 [2]: (CSE115 or EAS230 or EAS240 or EAS999)
CSE191 [3]: (CSE115 or EAS230 or EAS240 or EAS999)
CSE250 [4]: CSE116 and (CSE191 or MTH311)
MTH311 [5]: No prerequisites
EAS230 [6]: No prerequisites
EAS240 [7]: No prerequisites
EAS999 [8]: No prerequisites
MTH142 [9]: No prerequisites
CSE331 [10]: MTH142 and CSE250 and (CSE191 or MTH311)
The goal
The task is to check whether this sequence of prereqs is satisfiable/sane. And if so, what would be a set of courses to take to satisfy all the pre-requisites. Once could argue that this might not be the most natural objective but it is simple enough so that the SAT formulas that we have to talk about are not too complicated.
The variables
For each $i\in [10]$, let $c_i$ be the variable corresponding to the course with ID $i$.
Variables in Lingeling
The variables in Lingeling have to be integers starting with $1$ and for the above examples we will just use $i$ instead of variable $c_i$ in Lingeling.
The CNF formula that represents this set of constraints is: \[(c_1 \vee c_6 \vee c_7 \vee c_8) \wedge c_2 \wedge (c_3 \vee c_5) \wedge c_4 \wedge c_9 .\]
The format that actually gets fed into the solver is given below. Identifiers/variables in the same row are ORed together, different rows are ANDed together.
1 6 7 8 (Take one of CSE115, EAS230, EAS240, EAS999)
2 (Must take CSE116)
3 5 (Take CSE191 or MTH311)
4 (Must take CSE250)
9 (Must take MTH142)
These set of clauses are fed into a SAT solver, which outputs a satisfying assignment: i.e. each variable is set to true or false and further, for this assignment all the constraints/clauses are satisfied.
An "assignment" assigns each $c_i$ to either true or false.
Assignments in Lingeling
If variable $i$ is set to true, then it is represented as $i$ and if it is set of false, then it is represented as $-i$.
A set of constraints is satisfiable if and only if the assignment as a whole evaluates to true. That is, at least one of the literals inside the clauses being ANDed together must be set to true. For an example, look below. One possible assignment is:
c1 = True c2 = True c3 = True c4 = True c5 = True c6 = True c7 = True c8 = True c9 = True Solver output: [1 2 3 4 5 6 7 8 9 0]Since every identifier is positive in the result output by the SAT solver, the solver's recommendation is to simply take all the courses on offer. And naturally, this is one way to satisfy the prereqs, although probably not the one you will want to choose.
The 0 does not represent a variable.
The 0 is used by the solver to indicate the end of the assignment sequence. 0 is never used to represent a variable.
c1 = True c2 = True c3 = False c4 = True c5 = True c6 = True c7 = True c8 = True c9 = True Solver output: [1 2 -3 4 5 6 7 8 9 0] (take every course except CSE191)
c1 = True c2 = True c3 = True c4 = True c5 = False c6 = True c7 = True c8 = True c9 = True Solver output: [1 2 3 4 -5 6 7 8 9 0] (take every course except MTH311)
c1 = True c2 = True c3 = True c4 = True c5 = False c6 = False c7 = False c8 = False c9 = True Solver output: [1 2 3 4 -5 -6 -7 -8 9 0] (take the minimum required courses, the route most people take)
Important
Note that in the last assignment, the solver only assigned true to one literal in each clause/row. And indeed, this is the bare minimum requirement for a set of clauses to be satisfiable.
Followup #1
Suppose you cannot take both CSE116 and CSE191 together.In CNF, this translates to adding the row (-2 -3) to the list of clauses or $\neg c_2 \vee \neg c_3$ to the CNF formula specified before.
For the sake of completeness, the CNF formula is now:
$(c_1 \vee c_6 \vee c_7 \vee c_8) \wedge c_2 \wedge (c_3 \vee c_5) \wedge c_4 \wedge c_9 \wedge (\neg c_2 \vee \neg c_3) $
and the solver input is
1 6 7 8 (Take one of CSE115, EAS230, EAS240, EAS999) 2 (Must take CSE116) 3 5 (CSE191 or MTH311) 4 (Must take CSE250) 9 (Must take MTH142) -2 -3 (Either don't take CSE116 or don't take CSE191)This is still satisfiable, since MTH311 is an option even if you can't take CSE191. One such assignment is given below.
c1 = True c2 = True c3 = False c4 = True c5 = True c6 = True c7 = True c8 = True c9 = True Solver output: [1 2 -3 4 5 6 7 8 9 0]
Followup #2
Suppose you cannot take both CSE116 and CSE250 together.Additional row in the list of clauses: -2 -4
Solver Input:
1 6 7 8 (Take one of CSE115, EAS230, EAS240, EAS999) 2 (Must take CSE116) 3 5 (CSE191 or MTH311) 4 (Must take CSE250) 9 (Must take MTH142) -2 -4 (Either don't take CSE116 or don't take CSE250)Solver output:
UNSATExplanation: We mentioned before that for a set of clauses to be satisfiable, at least one literal in each row must be set to true. However, we added a constraint that forbids the solver from assigning both 2 and 4 to true. However, 2 and 4 are the only literals in their rows in the set of clauses. Consequently, they must be set to true if the sequence is to be satisfiable.
Followup #3
Suppose you cannot take both CSE116 and CSE191 and neither can you take MTH311 and CSE116 together.Additional row #1 in the list of clauses: -2 -3
Additional row #2 in the list of clauses: -2 -4
Solver Input:
1 6 7 8 (Take one of CSE115, EAS230, EAS240, EAS999) 2 (Must take CSE116) 3 5 (CSE191 or MTH311) 4 (Must take CSE250) 9 (Must take MTH142) -2 -3 (Either don't take CSE116 or don't take CSE191) -2 -4 (Either don't take CSE116 or don't take CSE250)Solver output:
UNSATExplanation: The same explanation as for the previous case still holds here.