Homework 3 Solution

    • Reduction

1.1    \Is it turtles all the way down?"

In lecture 11, we talked about how one can use the powerful tool of reduction to show that the Trav-eling Salesman Problem(TSP) is NP-complete assuming that we already know Hamiltonian cycle is NP-complete. However, how do we know Hamiltonian cycle is NP-complete in the rst place? What’s the beginning of this chain of reductions?


De nition 1.1 (informal) SAT(Boolean satis ability problem) asks whether the variables of a given Boolean Expression can be replaced by the values TRUE or FALSE in such a way that the expression evaluates to TRUE. If this is the case, the expression is called satis able.


    • our beloved Python 2 is retiring: https://pythonclock.org


1
v0.3



CS 5112    Algorithms and Data Structures for Applications    Fall 2019



For example, the expression A& B is satis able because one can nd the values A = TRUE, B = FALSE, which make A& B = TRUE. In contrast, A& A is unsatis able because this expression is FALSE for all possible variable assignments. 2

[Cook, 1971] and [Levin, 1973] proved that SAT is NP-complete, and that is the rst problem proven NP-completeness.

1.2    How might we proceed then?

Since the SAT problem is NP-complete, only algorithms(solvers) with exponential worst-case com-plexity are known, bad news. One idea to make progress is, can we reduce the users arbitrary-looking Boolean Expression to a simpler notation/form? That would simplify the solvers job.

De nition 1.2 CNF: Conjunctive Normal Form A Boolean Expression is in conjunctive normal

form (CNF) if it is a conjunction(AND: &) of one or more clauses, where a clause is an OR(j) of literals; otherwise put, it is an AND of ORs.3
*Form:

CNF Expression = AND (&) of clauses, e.g.(AjB)&(CjDjE) is a CNF Expression with 2 clauses

clause = OR (j) of literals, e.g.(AjBjC) is a clause of 3 literals; A alone can also be a clause with just 1 literal

literal = A(positive literal), A (negative literal, meaning NOT A) symbol = A, B, P, Q etc. 4

CNF examples: All of the following expressions in the variable symbols A, B, C, D, E, and F are in conjunctive normal form:

(AjBj  C)&(DjEjF)

(AjB)&C

AjB (viewed as a conjunction with just one clause AjB)

A&B (viewed as a conjunction of 2 single-literal clauses, A, B)

A

non-examples: The following expressions are not in CNF:

(BjC), since an OR is nested within a NOT (A&B)jC
A&(Bj(D&E)) , since an AND is nested within an OR

However, every Boolean Expression can be equivalently converted into CNF. For the three non-examples just mentioned, they are respectively equivalent to the following three CNF Expressions:

B&   C

(AjC)&(BjC)

A&(BjD)&(BjE)


2Why study SAT? The decision problem of SAT is of central importance to elds like Arti cial Intelligence(constraint solving, planning), cryptography etc. not only in theory, but also has huge impacts in real-life softwares (con g management-inside your favourite IDE, model checking etc.)
    • This is equivalent to the POS (Product of sums) form if you are familiar with digital electronics.

    • In our homework Python code we restrict the symbols that represents Boolean variables to be uppercase, so ’a’ cannot be used but ’A’ can to form an Boolean Expression


2
v0.3



CS 5112    Algorithms and Data Structures for Applications    Fall 2019



Reduction to CNF 5 In order to reduce the SAT problem into the CNF-SAT(whose de nition is very similar to SAT except that the Boolean Expression is in Conjunctive Normal Form) problem, we need to convert any arbitrary Boolean Expression into CNF, and we do so by a reduction gadget (the to_cnf_gadget in sat_solver.py), which conducts the following procedure6 while making sure each step does not change the meaning of the original expression.

Eliminate implications and equivalences:

{ step1 = parse_iff_implies(input)

A$B=(A!B)&(B!A)

A ! B =  AjB

Move NOTs inwards by recursively applying De Morgan’s Law 7 { step 2 = deMorgansLaw(step1)

(  A)=A

(AjB) = A& B (A&B) = Aj B
Distribute AND over OR, recursively { step3 = distibutiveLaw(step2)
(A&B)jC = (AjC)&(BjC)

Example In the python reduction gadget we are implementing, we only consider the following op-erators: AND(&, ^), OR(j, _), NOT( ), IMPLIES(==>), IFF(<=>).

For example, the input (P ! Q)j(R ! P) is represented in the rst row of the table below, and each row after that shows the expected return value when each step returns.
















After running distributiveLaw(), the expression has been reduced to CNF form:( QjPj R)&(PjPj R) and ready to be processed by a CNF-SAT solver.


    • The reduction described is polynomial time. And since we have reduced the original SAT problem to the CNF-SAT problem through this reduction, we now know CNF-SAT is NP-hard. Additionally CNF-SAT is in NP so CNF-SAT is still NP-complete.
6[Russell and Norvig, 2009]
7CNF requires NOT to appear only in literals, so we \move NOT inwards" repeatedly






3
v0.3



CS 5112    Algorithms and Data Structures for Applications    Fall 2019



1.3    Notes on the Python implementation

operators Here is a table of the operators that can be used to form Boolean Expressions. Note that the syntax for implication and equivalence is a bit funny but we are using it to overload the operators in Python.8














Non-deterministic return values SAT_solver’s return value is non-deterministic and non-exhaustive when its input expression is satis able, it will only return one satisfying assignment when it succeeds 9. The (P ! Q)j(R ! P) example above also shows this: there exists multiple satisfying assignments for that expression.

Todos

In sat_solver.py:

{ implement parse_iff_implies() ,

{ implement deMorgansLaw()in sat_solver.py

{ implement distibutiveLaw() in sat_solver.py

Once the above are implemented correctly, you should be able to run python3 sat_solver.py with no errors


1.4    Epilogue: SAT solvers and implications

Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known. The good news, however, is that e cient(although exponential) algorithms for SAT do ex-ist, among which DPLL([Davis et al., 1962]) is one of the most well-known. What DPLL does is to systematically backtrack and explore the (exponential sized) space of possible variable assignments looking for the satisfying ones.

Most SAT solvers today are essentially CNF-SAT solvers(our dpll as well) that forces you to enter a CNF Expression. To use an arbitrary Boolean Expression as input, you have to convert it to CNF yourself and that’s why the CNF converter we are implementing is useful. 10


8We do have a small problem to get around: we want to use Python’s built-in operators to express the Expressions in a simple and readable way. But Python does not allow implication arrows(==>) as operators, so we are forced to use a more verbose notation: |‘==>’| instead of just ==>. Alternatively, you can always use the Expr constructor forms
9We do this just to facilitate testing, the decision problem of SAT only asks us YES(satis able) or NO(unsatis able)

    10 Some SAT solvers could be even more restrictive: They could require each CNF clause to have at most 3 literals, which means they are essentially 3-CNF-SAT solvers






4
v0.3



CS 5112    Algorithms and Data Structures for Applications    Fall 2019













As it turns out, reducing SAT to CNF-SAT is actually quite useful in that we can further reduce CNF-SAT to more interesting and even seemingly unrelated problems and prove their NP-Completeness11.

    • Testing

To ensure compatibility with our grading software, please ensure that python3 sat_solver.py run without errors.

Just like previous homework, these tests are non-exhaustive meaning passing these tests alone does not necessarily guarantee a perfect score.

In addition to the provided tests, we encourage you to write additional tests and your own test cases. We are not providing the entire test harness for you because no one will do that for you in real-life development, you’ll have to write tests yourself.


































    11 see [Karp, 1972] if you are interested


5
v0.3



REFERENCES    REFERENCES



References

[Cook, 1971] Cook, S. A. (1971). The complexity of theorem-proving procedures. In Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC ’71, pages 151{158, New York, NY, USA. ACM.

[Davis et al., 1962] Davis, M., Logemann, G., and Loveland, D. (1962). A machine program for theorem-proving. Commun. ACM, 5(7):394{397.


[Karp, 1972] Karp, R. M. (1972). Reducibility among Combinatorial Problems, pages 85{103. Springer US, Boston, MA.

[Levin, 1973] Levin, L. A. (1973). Universal sequential search problems. Problems of Information Transmission, 9(3):265{266.

[Russell and Norvig, 2009] Russell, S. and Norvig, P. (2009). Arti cial Intelligence: A Modern Ap-proach. Prentice Hall Press, Upper Saddle River, NJ, USA, 3rd edition.













































6