Resolution

Your assignment for this week is to implement a SAT solver. In the SAT lab, we implemented a DPLL SAT solver which focuses on finding an answer when the formula is satisfiable. For this assignment, we will implement another SAT solver which focuses on finding an answer when the formula is unsatisfiable. While DPLL provides a truth assignment that satisfies the formula (if it is satisfiable), this algorithm does not. Instead, it can provide a proof why a formula is unsatisfiable (if it is).

Background

Basic Definitions

• A literal is a positive or negative occurrence of a boolean variable.
• A clause is a disjunction of set of literals. We will write {p, q, r} to represent $p \lor q \lor r$. A special case is an empty clause, which is false as you saw in the SAT lab.
• A clause set represents a CNF formula in the algorithm to solve the SAT problem. It is a conjunction of sets of clauses, although we will treat it as a set.

Overview

Given a CNF formula, we would like to know if the formula is unsatisfiable. If it is unsatisfiable, we want to obtain a proof of its unsatisfiability. Note that false is a consequence of an unsatisfiable formula. Therefore, given the formula, false should be provable or derivable in a "powerful enough deductive system". The motivation to work in a deductive system is that we will obtain a proof automatically. For those who are interested in the theory behind deductive system, please see the appendix.

To give an overview of what we are going to do: the algorithm to solve the SAT problem will use a deductive system with one rule called the resolution rule, which is powerful enough to derive false from any unsatisfiable clause set. So, given the formula, if we are able to derive false, we can conclude that the formula is unsatisfiable. If we cannot derive false, then we conclude that the formula is satisfiable.

The core of the algorithm is the resolution rule, which states that:

For any two clauses $\alpha$, $\beta$ where $\alpha$ contains a positive literal $p$ and $\beta$ contains a negative literal $-p$. That is, we have $\alpha = \{a_1, a_2, ..., a_x, p\}$ and $\beta = \{b_1, b_2, ..., b_y, -p\}$ where $a_i$ and $b_i$ are literals (could be positive or negative). Then, you will be able to derive {$a_1, a_2, ..., a_x, b_1, b_2, ..., b_y$}.

This formula {$a_1, a_2, ..., a_x, b_1, b_2, ..., b_y$} is known as the resolvent. Notice a special case of this rule when $x = y = 0$. After resolving $\alpha$ and $\beta$, the resolvent would be {} which is false. In the algorithm, this would lead to a conclusion that the formula is unsatisfiable.

Algorithm

• First, add all clauses to the clause set.
• For each variable $p$, eliminate it by:
  • Resolve using variable $p$ with all two clauses that are possible and add them to the clause set. That is, for all two clauses $\alpha$ and $\beta$ in the clause set where $\alpha$ contains positive literal $p$ and $\beta$ contains negative literal $-p$, resolve $\alpha$ and $\beta$ and add the resolvent to the clause set. Repeat this until nothing can be resolved anymore with variable $p$ (see question 3 regarding an optimization which you could use in your implementation).
  • All clauses that contain a variable $p$ are now completely carried by all resolvents (see the appendix for a rigorous explanation). So, we no longer need any clauses that contain the variable $p$. Remove these clauses from the clause set.
  • If an added resolvent is {}, we know that the formula is unsatisfiable.
• After the loop finishes, because we did not declare that the formula is unsatisfiable, we can conclude that it is satisfiable.

Suppose the formula is unsatisfiable, the history of all resolutions that we have performed tells how to derive false from the formula. This precisely is the proof for why the formula is unsatisfiable, just like how you prove a theorem in mathematics.

Example

Example 1

Given a formula {{a, b}, {-a}, {-b}, {c, -a}, {a, d}}. We would like to know if it is unsatisfiable or not:

1. Initially, the clause set has {{a, b}, {-a}, {-b}, {c, -a}, {a, d}}
2. Eliminate variable a by:
   1. Resolve {a, b} and {-a}. Add the result {b} to the clause set.
   2. Resolve {a, b} and {c, -a}. Add the result {b, c} to the clause set.
   3. Resolve {-a} and {a, d}. Add the result {d} to the clause set.
   4. Resolve {c, -a} and {a, d}. Add the result {c, d} to the clause set.
   5. Now we have {{a, b}, {-a}, {-b}, {c, -a}, {a, d}, {b}, {b, c}, {d}, {c, d}}. Eliminate all clauses that have variable a or -a. Now we have {{-b}, {b}, {b, c}, {d}, {c, d}}
3. Eliminate variable d by:
   1. There are no clauses to resolve.
   2. Eliminate all clauses that have variable d or -d. Now we have {{-b}, {b}, {b, c}}.
4. Eliminate variable b by:
   1. Resolve {-b} and {b}. The result is {}, so the original formula is unsatisfiable.
   2. (Optional) Extract the proof, which is the history of all resolutions.

Assignment (Part 1)

Implement a SAT solver using this algorithm.

Input Specification

This is exactly like the SAT lab. Your program should take in a formula from standard input, where a formula is a list of clauses separated by newlines and each clause is a list of literals separated by spaces. Literals are represented as non-zero numbers where a positive number denotes a positive literal and a negative number denotes a negative literal. There is an implicit "or" between each literal and an implicit "and" between clauses.

For example:

-1 2
2 3

represents an input formula with two clauses. The first says that either variable 1 is false or variable 2 is true; the second says that either variable 2 or variable 3 is true.

You may assume that the input is well-formed and that your program will not be given any literal that wouldn't fit in a 32-bit signed integer.

Output specification:

If a formula is unsatisfiable, your program should output the string unsat, otherwise it should output the string sat.

Testing

To make sure your program conforms to our input output specifications we are providing you with a very simple testing script. You should make sure that your program passes this test because if it doesn't we won't be able to run our autograder and you will receive a zero for the implementation portion of the assignment. Note that this script does not test your program for correctness! You should do your own testing to ensure that your program is correct.

To run the script you can enter cs1950y_res <path-to-your-resolution-executable>

Assignment (Part 2)

Answer the following questions in a file named quiz.txt

Question 1

Verify that the resolution rule is sound by writing a truth table for it. Use & for and, | for or, - for negation, and -> for implication.

As an example, Modus Ponens states, for any two formulas A and A -> B, we will be able to derive B. Therefore we would check for (A & (A -> B)) -> B:

A	B	A -> B	A & (A -> B)	(A & (A -> B)) -> B
T	T	T	T	T
T	F	F	F	T
F	T	T	F	T
F	F	T	F	T

So the rule Modus Ponens is sound.

For simplicity, you should consider a special case of resolution rule where you resolve p | q and -p | r to derive q | r.

Question 2

Unlike DPLL, this algorithm does not use backtracking. Why can the runtime of this algorithm be exponential?

Question 3

If you have a clause containing both p and -p for some variable p, what optimization could you make?

Question 4

If a formula is satisfiable, what will be in the clause set when the algorithm is finished?

Handing In

To handin run cs1950y_handin resolution from a directory holding your 2 files (an executable named resolution and a text file named quiz.txt). You should receive an email confirming that your handin has worked. Resolution is due on 3/23 at 11:59pm.

Appendix (Optional)

Here!