NP-complete problems

• Decision (yes/no) problems
• Can be verified quickly (in polynomial time)
• Currently unknown how to solve quickly (P versus NP problem)
• All equivalent!

Examples

• Knapsack
• Travelling salesman
• Subset sum
• Graph coloring
• Sudoku
• Boolean satisfiability

Boolean satisfiability problem

Can we assign truth values to Boolean variables in propositional logic formulas to satisfy the formula?

Boolean satisfiability problem

• Commonly expressed like \((x \vee y \vee z) \wedge (x \vee \neg y) \wedge (\neg y \vee \neg x) \wedge (\neg z)\) (Conjunctive Normal Form)
• NP-complete (!)
• Can express any other NP-complete problem!

SAT solvers

Programs that solve boolean satisfiability problems and tell you satisfying assignments!!

Example

Tim Stellmach, CC0, via Wikimedia Commons

Rules

• one digit per cell
• each digit once per row/column
• each digit once per 3x3 sub-grid
• must use filled-in cells

Insight

• 9 boolean variables for each cell!
• only 1 is true, other 8 are false
• \(x_{r,c,1}\), \(x_{r,c,2}\),…,\(x_{r,c,9}\)

Each cell has at least one value

\[\displaylines{ \definecolor{comment}{RGB}{161,161,180} {\color{comment}\textit{\tiny{row 1, column 1 is one of 1,2,...9}}} \\ (x_{1,1,1} \vee x_{1,1,2} \vee \dots \vee x_{1,1,9}) \wedge \\ {\color{comment}\textit{\tiny{row 1, column 2 is one of 1,2,...9}}} \\ (x_{1,2,1} \vee x_{1,2,2} \vee \dots \vee x_{1,2,9}) \wedge \\ \dots \\ {\color{comment}\textit{\tiny{row 9, column 9 is one of 1,2,...9}}} \\ (x_{9,9,1} \vee x_{9,9,2} \vee \dots \vee x_{9,9,9}) }\]

Each row has all values

\[\displaylines{ \definecolor{comment}{RGB}{161,161,180} {\color{comment}\textit{\tiny{row 1 has a 1}}} \\ (x_{1,1,1} \vee x_{1,2,1} \vee \dots \vee x_{1,9,1}) \wedge \\ {\color{comment}\textit{\tiny{row 1 has a 2}}} \\ (x_{1,1,2} \vee x_{1,2,2} \vee \dots \vee x_{1,9,9}) \wedge \\ \dots \\ {\color{comment}\textit{\tiny{row 9 has a 9}}} \\ (x_{9,1,9} \vee x_{9,2,9} \vee \dots \vee x_{9,9,9})}\]

Each cell has at most one value

\[\displaylines{ \definecolor{comment}{RGB}{161,161,180} {\color{comment}\textit{\tiny{row 1, column 1 is not both 1 and 2}}} \\ (\neg x_{1,1,1} \vee \neg x_{1,1,2}) \wedge \\ {\color{comment}\textit{\tiny{row 1, column 1 is not both 1 and 3}}} \\ (\neg x_{1,1,1} \vee \neg x_{1,1,3}) \wedge \\ \dots \\ {\color{comment}\textit{\tiny{row 9, column 9 is not both 8 and 9}}} \\ (\neg x_{9,9,8} \vee \neg x_{9,9,9})}\]

Solving

1. Express your problem as a propositional logic formula in CNF
2. Feed it to a SAT solver
3. ????
4. PROFIT!!!

Example

\[(x \vee y \vee z) \wedge (x \vee \neg y) \wedge (\neg y \vee \neg x) \wedge (\neg z)\]

\(x\): 🤷
\(y\): 🤷
\(z\): 🤷

Pick a variable

Let’s set \(z\) to False

Unit propagation

• If there is a unary clause, assign it
• Delete all clauses that are satisfied
• Remove the literal where it is False

Example

\[(x \vee y \vee \cancel{{\color{red} z}}) \wedge (x \vee \neg y) \wedge (\neg y \vee \neg x) \wedge \cancel{{\color{green} (\neg z)}}\]

\(x\): 🤷
\(y\): 🤷
\(z\): False

Pick a variable

Let’s set \(y\) to True

Example

\[\cancel{{\color{green}(x \vee y \vee z)}} \wedge (x \vee \cancel{{\color{red} \neg y}}) \wedge (\cancel{{\color{red} \neg y}} \vee \neg x) \wedge \cancel{{\color{green}(\neg z)}}\]

\(x\): 🤷
\(y\): True
\(z\): False

Conflict!

\[\cancel{{\color{green}(x \vee y \vee z)}} \wedge ({\color{blue} x} \vee \cancel{{\color{red} \neg y}}) \wedge (\cancel{{\color{red} \neg y}} \vee {\color{blue}\neg x}) \wedge \cancel{{\color{green}(\neg z)}}\]

\(x\): 🤷
\(y\): True
\(z\): False

Backtrack

Let’s set \(y\) to False

Example

\[(x \vee \cancel{{\color{red} y}} \vee \cancel{{\color{red} z}}) \wedge \cancel{{\color{green}(x \vee \neg y)}} \wedge \cancel{{\color{green} (\neg y \vee \neg x)}} \wedge \cancel{{\color{green} (\neg z)}}\]

\(x\): 🤷
\(y\): False
\(z\): False

Pure literal elimination

There is only one possible value for \(x\), so assign it

Solution

\[\cancel{{\color{green}(x \vee y \vee z)}} \wedge \cancel{{\color{green}(x \vee \neg y)}} \wedge \cancel{{\color{green} (\neg y \vee \neg x)}} \wedge \cancel{{\color{green} (\neg z)}}\]

\(x\): True
\(y\): False
\(z\): False

Davis-Putnam-Logemann-Loveland

• Backtracking search
• Unit propagation
• Pure literal elimination

Downsides

• Often finds the same conflict multiple times
• Backtracks one level at a time (chronologically)
• No memory of past conflicts

Can we learn from our mistakes?

CDCL

• Distinguishes between decisions (assignments) and implications (unit propagation, pure literal elimination)
• Keeps track of the implication graph

Example

\[\begin{align} & (a \vee d) \wedge \\ & (a \vee \neg c \vee \neg f) \wedge \\ & (a \vee f \vee j) \wedge \\ & (b \vee i) \wedge \\ & (\neg e \vee \neg c \vee g) \wedge \\ & (\neg e \vee f \vee \neg g) \wedge \\ & (e \vee f \vee \neg h) \wedge \\ & (e \vee h \vee \neg j) \end{align}\]

\(a\)

\[\begin{align} & {\color{red} a} \vee {\color{green} d} \\ & {\color{red} a} \vee \neg c \vee \neg f \\ & {\color{red} a} \vee f \vee j \\ & b \vee i \\ & \neg e \vee \neg c \vee g \\ & \neg e \vee f \vee \neg g \\ & e \vee f \vee \neg h \\ & e \vee h \vee \neg j \end{align}\]

\(c\)

\[\begin{align} & {\color{red} a} \vee {\color{green} d} \\ & {\color{red} a} \vee {\color{red}\neg c} \vee {\color{green} \neg f} \\ & {\color{red} a} \vee {\color{red} f} \vee {\color{green} j} \\ & b \vee i \\ & \neg e \vee {\color{red}\neg c} \vee g \\ & \neg e \vee {\color{red} f} \vee \neg g \\ & e \vee {\color{red} f} \vee \neg h \\ & e \vee h \vee {\color{red}\neg j} \end{align}\]

\(b\)

\[\begin{align} & {\color{red} a} \vee {\color{green} d} \\ & {\color{red} a} \vee {\color{red}\neg c} \vee {\color{green} \neg f} \\ & {\color{red} a} \vee {\color{red} f} \vee {\color{green} j} \\ & {\color{red} b} \vee {\color{green} i} \\ & \neg e \vee {\color{red}\neg c} \vee g \\ & \neg e \vee {\color{red} f} \vee \neg g \\ & e \vee {\color{red} f} \vee \neg h \\ & e \vee h \vee {\color{red}\neg j} \end{align}\]

\(e\)

\[\begin{align} & {\color{red} a} \vee {\color{green} d} \\ & {\color{red} a} \vee {\color{red}\neg c} \vee {\color{green} \neg f} \\ & {\color{red} a} \vee {\color{red} f} \vee {\color{green} j} \\ & {\color{red} b} \vee {\color{green} i} \\ & {\color{red}\neg e} \vee {\color{red}\neg c} \vee {\color{blue} g} \\ & {\color{red}\neg e} \vee {\color{red} f} \vee {\color{blue}\neg g} \\ & {\color{green} e} \vee {\color{red} f} \vee \neg h \\ & {\color{green} e} \vee h \vee {\color{red}\neg j} \end{align}\]

Unique Implication Point

\[\displaylines{\neg (\neg f \wedge c \wedge e) \\ \iff \\ (f \vee \neg c \vee \neg e)}\]

Learned clause

\[(f \vee \neg c \vee \neg e)\]

Learned clause

\[\begin{align} \definecolor{comment}{RGB}{161,161,180} \definecolor{emphasis}{RGB}{88,110,117} & {\color{comment}(a \vee d) \wedge} \\ & {\color{comment}(a \vee \neg c \vee \neg f) \wedge} \\ & {\color{comment}(a \vee f \vee j) \wedge} \\ & {\color{comment}(b \vee i) \wedge} \\ & {\color{comment}(\neg e \vee \neg c \vee g) \wedge} \\ & {\color{comment}(\neg e \vee f \vee \neg g) \wedge} \\ & {\color{comment}(e \vee f \vee \neg h) \wedge} \\ & {\color{comment}(e \vee h \vee \neg j) \wedge} \\\ & (f \vee \neg c \vee \neg e) \end{align}\]

Backjumping

Conflict-driven Clause Learning

• Learned clauses!
• Non-chronological backtracking!
• Basis of most modern SAT solvers

Okay now let’s do a silly one

What if we just guessed?

1. Generate a random assignment
2. Pick a random clause
3. Probabilistically flip a variable in the clause
4. Repeat until you solve it or get tired!

Stochastic Local Search

• Surprisingly effective!
• WalkSAT
• Can be done in parallel
• Can use a form of clause learning
• Can’t conclusively determine unsatisfiability(!)
• Reminds me of simulated annealing in some ways

Problem

\[ \begin{align} SEND &\\ + MORE &\\ \hline MONEY \end{align} \]

How?

We’d have to teach the SAT solver arithmetic!

Satisfiability Modulo Theories

• SAT solvers extended
• bitvectors, arrays, algebraic datatypes, etc.
• Z3, CVC, Yices, Boolector

SAT solvers

Solve NP-complete problems expressed as CNF Boolean formulas

DPLL

• Backtracking search
• Unit propagation
• Pure literal elimination

CDCL

• DPLL++
• Learned clauses
• Non-chronological backtracking

SLS

• Random guessing
• Probabilistic variable flipping

SMT solvers

SAT extended with theories

Resources

• Lindsey Kuper - Reasoning Under Uncertainty in SMT Solving, Research, and Life
• The Science of Brute Force
• Handbook of Satisfiability
• GRASP - A New Search Algorithm for Satisfiability (1996)
• An Extensible SAT-solver (2003)
• CS-E3220: Propositional satisfiability and SAT solvers

Slides

https://vaibhavsagar.com/presentations/sat-solvers