Sat Solver

Due: Wed Oct 02 11:59 pm
Starter files: lab4.zip
Submission: Please submit your work using Gradescope.

Overview

The learning goals of this lab are the following:

further hone recursive thinking
gain familiarity with important concepts in propositional logic: conjunctive normal form, satisfiability
implement an algorithm to solve one of the most important problems known to mankind

Background

In this lab, you are asked to implement an algorithm that takes as input a proposition that is written in Conjunctive Normal Form (CNF) and returns true if the proposition has a satisfying assignment and false if the proposition is unsatisfiable.

This is a very important problem, as discussed in the reading (see Ch. 3.3.3 and the “CS Connection” on p. 326). In fact, you might say this is the most important problem in all of computer science. Many real-world problems can cast as CNF satisfiability problems. For example, it is used to check Paris Metro railway control system for bugs.

Algorithm Overview

Here’s a high level description of the algorithm you should implement. First, you maintain a model, which is a partial assignment of variables to truth values. Initially, the model is empty, meaning no variable has been assigned a truth value. As the algorithm progresses, variables are assigned to truth values and the model is udpated accordingly. (You can think of the model as a dictionary (or map) that maps a variable name to a boolean (true or false).) If the proposition evaluates to true under the model, then you have found a satisfying assignment, and the algorithm should return true.

Your job is to systematically search the set of all possible assignments to see if one of them is a satisfying assignment.

Before explaining how, let’s define a helper method.

Let’s define isSatHelper as follows. It takes a proposition $\varphi$ and a model $M$ and returns true when the proposition can be satisfied under model $M$. Here are some example inputs and outputs.

Input: $\varphi := (p \lor q) \land (\lnot q)$ and $M := { p \rightarrow \text{T} }$ ($p$ is assigned to True). Output: True because $\varphi$ is satisfiable under model $M$, we can set $q$ to False and the proposition is True.
Input: $\varphi := (p \lor q) \land (\lnot q)$ and $M := { p \rightarrow \text{F} }$. Output: False because the model forces $p$ to be False and regardless of how we set $q$, the propsition will be False.
Input: $\varphi := (p \lor \lnot q \lor \lnot r)$ and $M := { p \rightarrow \text{F}, q \rightarrow \text{T} }$. Output: True because if we set $r$ to False, the propsition evaluates to True.
Input: $\varphi := (p \lor \lnot q \lor \lnot r)$ and $M := { p \rightarrow \text{F}, q \rightarrow \text{T}, r \rightarrow \text{T} }$. Output: False. Even though $\varphi$ is satisfiable in general, it is not under this model $M$.

We can implement isSatHelper using recursion.

The basic idea is this: suppose $p$ is a variable that appears in the proposition $\varphi$ but has not yet been assigned a truth value in the model $M$. Let’s try setting $p$ to true and seeing if the proposition is satisfiable.

By assigning $p$ to true, we have made the problem “smaller”: there is one less variable to consider. After we assign $p$ to true, we can make a recursive call. If assigning $p$ to true does not yield a satisfying assignment, then we set $p$ to false and see if it’s satisfiable (with another recursive call). If we try setting $p$ to both true and false, and neither yields a satisfying assignment, then the proposition must be unsatisfiable.

The base case occurs when the model is “complete”: every variable in $\varphi$ has been assigned a value in model $M$. In this case, you check whether the proposition evaluates to true under this assignment. If it does, you’ve found a satisfying assignment! If not, this particular model does not lead to a satisfying assignment, so return False.

Pseudocode

Here is a pseudocode description of the recursive algorithm:

def isSatHelper(proposition, model):
  # base case
  # ---------
  # check the model: have all variables been assigned?
  if all variables have been assigned:
    if proposition evaluates to true:
      # you have found a satisfying assignment!
      return True
    else:
      # this particular assignment does not satisfy the proposition
      return False

  # recursive case
  # --------------
  var = choose any unassigned variable

  # try setting var to True, see if this leads a satisfying assignment
  update model, assigning var to True
  if isSatHelper(proposition, model):
    return True

  # try setting var to False
  update model, assigning var to False
  if isSatHelper(proposition, model):
    return True

  # looks like we don't have a satisfying assignment
  update model, unassign var
  return False  # proposition is unsatisfiable

Your tasks

I suggest you complete tasks in the following order.

Briefly review the following classes: Variable, Literal, Clause, and Model. You do not need to modify these classes. You should know what each class represents and what public methods are available for you to use. You don’t necessarily need to understand how each method works.
In CNFProposition, implement the getVariables() method. See the comment for hints on how to proceed. This should only take a few minutes. If you’re stuck, ask for help.
Implement SatSolver.isSatisfiableHelper based on the provided pseudocode description. You are encouraged to break the problem down and write your own helper methods in SatSolver.
Test your implementation! Code is provided to allow you to make arbitrary CNF propositions and call your code on them. See SatSolver.main for examples.