Class 6: SAT Solving
Schedule
Problem Set 2 is due Friday at 6:29pm. A few of the problems on PS2 are quite challenging! The problems are organized by topic, not by difficulty (the hardest problems are #4 and #7). I hope everyone makes a good attempt to solve all of the problems, but don’t be overly stressed if you cannot solve these ones and move on to the other problems if you are stuck on them (to hopefully return to these problems after you’ve had more time to think about them). Good solutions to these problems will impress us, but are not necessary to get a good score on PS2.
I will be out-of-town Monday, and not able to hold my usual office hours on Monday. I will have “make-up” office hours on Wednesday, 3:30-4:30pm (in addition to my usual Wednesday 1-2pm office hours).
Links
Sahand Saba’s Understanding SAT by Implementing a Simple SAT Solver in Python [Code with my modifications: https://github.com/evansuva/simple-sat]
XKCDs on NP-Complete problems: Subset Sum, Travelling Seller
Pancakes, Puzzles, and Polynomials: Cracking the Cracker Barrel (reducing pegboard puzzle to 3SAT)
Notes and Questions
Definition. A formula is in 3SAT if it is in 3CNF form and it is satisfiable.
$$ (x_1 \vee x_2 \vee x_3) \wedge (x_1 \vee \overline{x_2} \vee x_3) \wedge (\overline{x_1} \vee x_2 \vee \overline{x_3}) $$
\begin{center} \tiny \begin{math} (x{48} \vee x{4} \vee \overline{x{9}}) \wedge (\overline{x{44}} \vee x{50} \vee \overline{x{37}}) \wedge (\overline{x{8}} \vee \overline{x{1}} \vee x{28}) \wedge (x{21} \vee x{27} \vee \overline{x{32}}) \wedge (x{17} \vee x{29} \vee \overline{x{30}}) \wedge (x{30} \vee x{24} \vee x{37}) \wedge (\overline{x{22}} \vee \overline{x{27}} \vee \overline{x{44}}) \wedge (x{8} \vee \overline{x{25}} \vee \overline{x{24}}) \wedge (\overline{x{44}} \vee x{50} \vee x{14}) \wedge (x{45} \vee x{15} \vee x{37}) \wedge (\overline{x{16}} \vee x{14} \vee \overline{x{36}}) \wedge (\overline{x{33}} \vee x{5} \vee x{26}) \wedge (x{18} \vee \overline{x{7}} \vee \overline{x{24}}) \wedge (x{31} \vee x{38} \vee x{28}) \wedge (x{31} \vee \overline{x{33}} \vee \overline{x{8}}) \wedge (x{49} \vee x{7} \vee \overline{x{6}}) \wedge (x{34} \vee \overline{x{8}} \vee x{46}) \wedge (x{4} \vee \overline{x{5}} \vee \overline{x{35}}) \wedge (x{43} \vee x{27} \vee x{39}) \wedge (\overline{x{46}} \vee \overline{x{40}} \vee \overline{x{27}}) \wedge (\overline{x{25}} \vee x{14} \vee \overline{x{49}}) \wedge (x{38} \vee x{5} \vee x{15}) \wedge (x{9} \vee x{14} \vee \overline{x{19}}) \wedge (x{45} \vee \overline{x{42}} \vee \overline{x{39}}) \wedge (x{34} \vee \overline{x{22}} \vee \overline{x{28}}) \wedge (\overline{x{20}} \vee x{15} \vee \overline{x{8}}) \wedge (\overline{x{44}} \vee \overline{x{10}} \vee \overline{x{9}}) \wedge (x{22} \vee \overline{x{31}} \vee x{14}) \wedge (\overline{x{9}} \vee \overline{x{42}} \vee \overline{x{15}}) \wedge (\overline{x{40}} \vee x{12} \vee \overline{x{32}}) \wedge (\overline{x{20}} \vee \overline{x{6}} \vee \overline{x{15}}) \wedge (\overline{x{37}} \vee x{39} \vee \overline{x{23}}) \wedge (\overline{x{3}} \vee \overline{x{40}} \vee \overline{x{32}}) \wedge (\overline{x{4}} \vee \overline{x{25}} \vee x{7}) \wedge (\overline{x{20}} \vee \overline{x{36}} \vee \overline{x{37}}) \wedge (\overline{x{40}} \vee \overline{x{35}} \vee x{39}) \wedge (\overline{x{43}} \vee \overline{x{40}} \vee \overline{x{7}}) \wedge (x{34} \vee x{44} \vee x{26}) \wedge (x{13} \vee x{27} \vee x{28}) \wedge (x{12} \vee \overline{x{36}} \vee x{7}) \wedge (\overline{x{16}} \vee x{9} \vee \overline{x{24}}) \wedge (\overline{x{48}} \vee x{14} \vee x{28}) \wedge (x{16} \vee x{4} \vee x{40}) \wedge (\overline{x{25}} \vee x{15} \vee x{37}) \wedge (x{47} \vee \overline{x{26}} \vee \overline{x{23}}) \wedge (x{4} \vee \overline{x{13}} \vee x{36}) \wedge (x{48} \vee \overline{x{13}} \vee \overline{x{37}}) \wedge (x{4} \vee x{35} \vee \overline{x{27}}) \wedge (\overline{x{22}} \vee x{47} \vee x{26}) \wedge (\overline{x{22}} \vee \overline{x{46}} \vee x{27}) \wedge (\overline{x{20}} \vee x{49} \vee x{11}) \wedge (x{42} \vee \overline{x{10}} \vee x{28}) \wedge (\overline{x{45}} \vee x{28} \vee \overline{x{37}}) \wedge (x{14} \vee \overline{x{32}} \vee \overline{x{23}}) \wedge (x{22} \vee x{14} \vee x{23}) \wedge (\overline{x{17}} \vee \overline{x{46}} \vee \overline{x{7}}) \wedge (\overline{x{31}} \vee x{46} \vee \overline{x{50}}) \wedge (x{34} \vee \overline{x{41}} \vee x{43}) \wedge (x{17} \vee \overline{x{9}} \vee x{15}) \wedge (x{46} \vee x{14} \vee \overline{x{12}}) \wedge (\overline{x{20}} \vee x{12} \vee x{14}) \wedge (x{41} \vee x{42} \vee \overline{x{15}}) \wedge (x{48} \vee x{46} \vee \overline{x{36}}) \wedge (\overline{x{22}} \vee \overline{x{4}} \vee \overline{x{49}}) \wedge (x{22} \vee x{12} \vee \overline{x{42}}) \wedge (x{13} \vee \overline{x{38}} \vee x{39}) \wedge (x{48} \vee \overline{x{16}} \vee \overline{x{27}}) \wedge (x{17} \vee \overline{x{18}} \vee \overline{x{26}}) \wedge (x{48} \vee \overline{x{40}} \vee \overline{x{35}}) \wedge (\overline{x{43}} \vee \overline{x{40}} \vee \overline{x{49}}) \wedge (x{29} \vee x{11} \vee \overline{x{32}}) \wedge (x{33} \vee \overline{x{17}} \vee x{39}) \wedge (\overline{x{25}} \vee \overline{x{9}} \vee \overline{x{6}}) \wedge (x{40} \vee \overline{x{50}} \vee x{19}) \wedge (x{8} \vee x{10} \vee \overline{x{27}}) \wedge (x{5} \vee x{9} \vee \overline{x{26}}) \wedge (x{45} \vee \overline{x{38}} \vee \overline{x{27}}) \wedge (\overline{x{4}} \vee \overline{x{40}} \vee \overline{x{42}}) \wedge (x{21} \vee x{50} \vee x{12}) \wedge (\overline{x{8}} \vee \overline{x{14}} \vee \overline{x{42}}) \wedge (\overline{x{17}} \vee x{47} \vee \overline{x{27}}) \wedge (x{49} \vee \overline{x{12}} \vee \overline{x{6}}) \wedge (x{27} \vee x{49} \vee \overline{x{32}}) \wedge (\overline{x{29}} \vee \overline{x{12}} \vee \overline{x{26}}) \wedge (x{48} \vee \overline{x{2}} \vee x{6}) \wedge (x{16} \vee x{36} \vee x{49}) \wedge (x{33} \vee \overline{x{12}} \vee \overline{x{26}}) \wedge (\overline{x{33}} \vee x{29} \vee x{49}) \wedge (\overline{x{48}} \vee x{2} \vee x{19}) \wedge (x{25} \vee x{36} \vee x{49}) \wedge (x{21} \vee x{40} \vee \overline{x{14}}) \wedge (\overline{x{34}} \vee \overline{x{44}} \vee \overline{x{6}}) \wedge (x{48} \vee \overline{x{50}} \vee \overline{x{1}}) \wedge (x{5} \vee \overline{x{12}} \vee x{7}) \wedge (x{21} \vee \overline{x{35}} \vee \overline{x{27}}) \wedge (\overline{x{22}} \vee \overline{x{16}} \vee \overline{x{14}}) \wedge (\overline{x{13}} \vee \overline{x{35}} \vee \overline{x{12}}) \wedge (\overline{x{4}} \vee \overline{x{35}} \vee \overline{x{42}}) \wedge (\overline{x{50}} \vee \overline{x{40}} \vee x{7}) \wedge (x{25} \vee x{47} \vee \overline{x{12}}) \end{math} \end{center}
Converting Truth Tables to CNF
\begin{tabular}{cc|cc}
$P$ & $Q$ & $P \implies Q$ & $P \oplus Q$ \ \hline
\T & \T & \T & \F
\T & \F & \F & \T
\F & \T & \T & \T
\F & \F & \T & \F
\end{tabular}
The output of the operator is \T\ if and only if the inputs do not match any row where the output is \F. We can ensure the inputs do not match a row, but OR-ing the negation of each input: in the disjunction, at least one must be \T\ to satisfy the clause.
Problems
Definition. A problem is a precise description of set of possible inputs and desired property of an output corresponding to each input.
Define the ADDITION problem (adding two integers):
#
Definition. A decision problem is a problem where the output is either T or F. Equivalently, we can view a decision problem as testing set membership: $x \in S$.
The SUM problem:
\begin{quote}
{\bf Input.} Three integers, $x$, $y$, and $z$.
{\bf Output.} \T\ iff $z = x + y$.
\end{quote}
How could we solve ADDITION using SUM?
##
Definition. A procedure is a precise description of an information process.
Definition. An algorithm for a particular problem is a procedure that solves that problem. To solve a problem, an algorithm must always (eventually) produce the correct output for any problem input.
Definition. A program is adescription of a procedure that can be executed by a computer.
Definition. The 3SAT decision problem takes as input a logical formula written in CNF, and outputs T if the input formula is satisfiable and outputs F otherwise.
How many uses of a solver for the 3SAT decision problem are sufficient to always find a satisfying assignment for a satisfiable formula?
##
SAT Solving (will be covered Tuesday)
Sahand Saba’s Understanding SAT by Implementing a Simple SAT Solver in Python (Code with a few modifications: https://github.com/evansuva/simple-sat)
What is the worst-case number of guesses needed to solve a SAT instance with $v$ variables and $c$ clauses using the ``brute-force guessing” strategy?
###
What is the worst-case number of guesses needed to solve a SAT instance with $v$ variables and $c$ clauses using the ``watchlists” strategy?
###
Why is it possible to solve most SAT instances reasonably quickly?