SAT

Due: 11:59pm ET Tuesday, April 7, 2020

SAT Solver

In this assignment, you will be implementing a DPLL SAT solver in the language of your choice.

The motivation for a SAT solver is to determine if, for a given boolean formula, there exists an assignment of true and false to the variables such that the entire formula evaluates to true. Algorithms that solve the boolean satisfiability problem are employed by Forge under the hood to determine the satisfiability of higher-level constraint models. In general, efficient SAT-solving is an extremely important and widely-used problem in computer science.

The DPLL algorithm works by choosing an assignment of true or false for a variable, simplifying the formula based on that choice, then recursively checking the satisfiability of the simplified formula.

Unit Clause Elimination

First, we'll implement unit propagation, which is one aspect of this formula simplification. For example:

-x

x y z

If a clause is a unit clause (one with only one variable), then the only way for the formula to be satisfiable is for that variable to be assigned consistently with its sign in that clause. Thus, we know that variable must take on that assignment, which tells us that all other clauses with that literal are now satisfied. In addition, we know that clauses with the literal's negation will not be satisfied by that component, so we can remove the negation from all clauses.

In our example above, -x is a unit clause, meaning our final solution must include the variable x evaluating to false. Any clause containing the variable -x is now satisfied, and any clause containing the variable (positive) x will never be true, unless the other variables in the clause containing positive x are satisfied (in the second clause, either y or z). In the example above we use letters to show it could be any variable, but remember in your solution the variables/input should be represented by numbers.

The pseudocode for unit clause elimination is included below.

for each unit clause {+/-x} in formula

remove all non-unit clauses containing +/-x

remove all instances of -/+x in every clause // flipped sign!

assign x consistent with its sign in unit clause

Pure Literal Elimination

The second aspect of formula simplification is eliminating pure literals (ones that occur with only one polarity throughout the formula). If a literal is pure, then each clause it appears in can be satisfied by assigning the variable consistent to the sign it appears with. Thus, without changing the satisfiability of the formula, we can add the pure literal as a unit clause and remove all other clauses it occurs in from the formula.

The pseudocode for pure-elim is included below.

for each variable x

if +/-x is pure in formula

remove all clauses containing +/-x

assign x consistent with its sign

Recursive Backtracking

After the DPLL employs these two simplification steps, it must pick some variable to branch on. The satisfiability problem is then split into two sub-problems: whether the formula is satisfiable with the chosen variable assigned as either true or false. Essentially, the algorithm "guesses" a variable to be true, recursively determines if that subproblem is satisfiable; if it is not, the algorithm then "guesses" the variable to be false and tries again.

You're free to choose any reasonable method of picking variables to branch on. You might randomly select a variable, pick the variable that occurs the most in the formula, or even just take the alphabetically-next variable. By "reasonable" we mean a method that leads to correct results.

The pseudocode for the recursive backtracking is included below.

func solve(varAssignment, formula):

// do unit clause elim and pure literal elim on the formula

unitClauseElim(formula)

pureLiteralElim(formula)

if formula has empty clause

return unsat

if formula has no clauses

sat -> return current varAssignment

x := pickVar(formula) // do anything reasonable here

if solve(varAssignment + {+x}, formula) is sat

return result of solving with x assigned to true

else

return solve(varAssignment + {-x}, formula)

Assignment

The assignment is to implement a SAT solver in the language of your choice following the I/O specifications given below. These follow the SAT competition standards (see sections 4.1 and 5.2).

Your solver should terminate in roughly under 30 seconds for inputs with fewer than 40 clauses and 25 variables. However, don’t stress too much about runtime if you go a bit over!

You should then try using your solver as the backend for Forge by opening up a Forge spec and adding the following line to the top of your spec. Make sure you update to the latest version of Forge (0.3.0) to have this feature available.

option solver “<path to your run.sh script>”

In four or so sentences, compare how quickly Forge is able to find an instance for some spec from a previous homework using your solver compared to the default one (with the above line removed). You can find the solve time (time spent in the actual SAT solver) in the debug information Forge prints before launching Sterling. Note down what spec you used and what the solve times were for a sat and unsat instance for your solver and for the default one.

Input Specification

Your SAT solver should adhere to the DIMACS standard. Your program should take one command line argument - the name of the input file. The input file will be in DIMACS format where it will have comment lines beginning with “c “, followed by a problem line of the form “p cnf <numVars> <numClauses>“. Following this, we have a list of clauses, each on its own line and ending in 0.

Non-zero integers represent literals, where a negative integer is the negated form of the variable. Each line is a clause (disjunction of literals), and, taken together, the clauses form the CNF problem that we want to find a satisfying assignment for.

c simple.cnf

p cnf 3 2

1 -3 0

2 3 -1 0

We should be able to run your SAT solver on an input file by running ./run.sh <file>.

Output Specification

Your SAT solver should output the solution by printing to standard output. If the problem is satisfiable, you should print “s SATISFIABLE” followed by a line starting with “v ” containing the variable assignment that satisfies the formula (where positive integers mean the variable was assigned to true and negative integers mean the variable was assigned to false). The “v” line should have 0 as the last character. You may optionally print additional lines as comment lines beginning with “c ”. For the above input example, the output might look like:

c solving simple.cnf

s SATISFIABLE

v 1 -3 2 0

c Finished in 1.950s

In this example, variables 1 and 2 are assigned to true and variable 3 is assigned to false.

If the input formula is unsatisfiable, you should print “s UNSATISFIABLE”.

Testing

We want you to prove to us that your SAT solver works. To this extent, it is crucial that you include some form of testing (both for individual functions and for the solver as a whole). Notice that there may be several different variable assignments that satisfy a particular formula, so you might consider testing properties of these outputs.

Language Choice

You may use any language of your choice for this assignment, provided you follow the I/O specifications above and you are able to run your solver on a department machine.

Stencil

We have provided stencil code that handles I/O for Java, Python, and Haskell located in /course/cs1950y/pub/sat, although you are free to use any language you wish. We have also provided the required run.sh script for each of these three languages. Feel free to modify the stencil in any way you see fit, provided you adhere to the I/O specifications above.

Collaboration Policy

You may receive debugging help from others per the project collaboration policy. In addition to high-level discussions, you may also receive debugging help from others (while their code is closed), but you must list the people you received assistance from in your collaborators file.

Handing In

For this assignment, you should hand in your source files (please delete stencils you didn’t use) as well as a run.sh script, which, when run, will invoke your SAT solver on a particular file. Also hand in your short write-up, writeup.txt. Please also submit a file named collaborators containing the logins of the people you received debugging help from (one on each line). Please do not include any identifying information for you or your partner in any of your files.

To handin, run cs1950y_handin sat from a directory containing these files. You should receive an email confirming that your handin has worked.