Project. Satisfiability test of clauses and its application

We have studied several methods to check (prove) the unsatisfiability of propositions. In the last decades, significant progress has been made to build efficient systems, also called SAT solvers, to test the satisfiability of a given proposition in Conjunctive Normal Form (we know that any proposition can be translated into CNF). SAT solvers have found wide applications including hardware/software verification problems, diagnosis and planning problems.


    • Objectives and deliverable

In this project, you are expected to
 

    • Download a SAT solver and know how to install it and use it on any Unix (or Linux) machine of our department.

    • Encode the n-queens (n is number input by users of your program) problem into the DIMACS CNF format and solve it by the SAT solver you have installed. Since the CNF format could be very large and complex, you may want to write a program to generate the CNF coding of the problem.

    • Write a compact while clear report on how you encode the problem into the CNF form. Don’t include your source code. You can use pseudo-code for your algorithm to gener-ate CNF for n queens.

    • Interview. There will be an interview of about 10 minute long. Our TA Vamsi will contact your team for the interview time later.
    • Background materials: file format and SAT solvers

The CNF input to a SAT solver is usually stored in a file with DIMACS CNF format. The input file starts with comments (each line starts with c). The number of variables and the number of clauses is defined by the line p cnf #variables #clauses. Each of the next lines specifies a clause: a positive literal is denoted by the corresponding number, and a negative literal is denoted by the corresponding negative number. The last number in a line should be zero. Here is an example.
c An example SAT formula:    ffA, : Bg, f: A, Bgg.

c We have 2 propositional letters (variables) A and B.

c We use number 1 for A and 2 for B.

c p CNF #variables #clauses

p CNF 2, 2

1, -2, 0

-1, 2, 0

You may use the SAT solver miniSAT (http://minisat.se/Main.html) or whatever solver you like. From the github page (whose link is on the miniSAT website main page) you can find how a binary miniSAT solver is used.


    • Apply logic and a proof procedure to solve interesting prob-lems

Here are some hints on encoding the n-queens problem into propositional logic. Consider 3 queens problem. We need to encode the following constraints 1) no two queens on the same row, 2) no two queens on the same column, and 3) no two queens on the same diagonal.

The objective is to find a formula whose satisfiable assignment gives us a solution to the n-queens problem. One idea is to introduce a proposition letter (variable) for each position on the 3X3 board. Let Pij denote the propositional letter for position (i; j) of the board. If Pij is true, there is a queen on (i; j); otherwise, there is no queen on (i; j).

To express the observation that there is a queen for first row:

P11 _ P12 _ P13:

To express the constraint that there is no two queens on the first row: if any P1i is true, then other P1j ’s of first row should be false, i.e.,

P11 ! :P12;
P11 ! :P13;
P12 ! :P11;
P12 ! :P13;
P13 ! :P11;
P13 ! :P12:

You know how to translate ! connective to _ connective.

2
You may note that to solve the n-queens problem, we are specifying the problem (using logic) instead of trying to find an algorithm to solve it. Once we work out the formula, the SAT solver can be employed to produce a solution to the formula (and thus the original prob-lem) automatically. This project shows how logic and the proof procedures can be applied to solve academic (and real life) problems.


























































3