The puzzling SAT puzzle

• You have a bunch of switches: $x_1, \dots, x_k$
• Each switch turn on/off different lights.
• You want to turn at least one light on in each line:

SAT as Propositional Logic

• Each switch is a Boolean variable $x$
  • true is switch on
  • false is switch off
• Each cell is a literal: either $x$ or $\neg x$
• Each row is a clause, ie a disjunction of literal: “at least one”
• The game = a conjunction of clauses, aka a CNF Formula

SAT is Hard

• Obvious method for SAT: try every combination of switches.
• Takes $2^n$ tries for $n$ switches. Does not scale.
• Surely there is a better algorithm?
  • in practice yes (stay tunned)
  • in theory, not sure… every known algorithm needs $2^{n - o(1)}$ steps.

SAT as a “Programming Language”

A reason for the hardness of SAT: its expressivity.

• We can encode many things with SAT.
• Sudoku example:
  • $x_{i,j}^k$ is true if entry $i,j$ is equal to $k$
  • $\neg x_{i,j}^1 \vee \neg x_{i,j}^2$: entry $(i,j)$ cannot be both set to $1$ and $2$
  • $x_{i,j}^1 \vee x_{i,j}^2 \vee \dots \vee x_{i,j}^9$: entry $(i,j)$ has at least one value.
  • $\neg x_{1,j}^k \vee \neg x_{1,p}^k$ for $p<j$: entries $(1,j)$ and $(1,p)$ cannot be both set at value $k$ (because they are on the same line)
  • $\dots$
• A solution to a Sudoku = a solution to the CNF formula.

Modeling reasoning

• Sudoku: specify constraints of the system and let the solver figures out an answer.
• Many systems are described through constraints.
• Configuration problems:
  • Define a set of “possible” products with options.
  • Physical, industrial, marketing constraints.
  • E.g.: bikes, computers, software (compilation options).
  • “Color gold only possible if fancy frame and fancy bell are choosen”: $(\neg x_{gold} \vee x_{fancyframe}) \wedge (\neg x_{gold} \vee x_{francybell})$
• We can use a more expressive language (“Constraint Satisfaction Problem”), see e.g. xcsp, which is often “compiled” into SAT before solving.

Modeling computation

We can actually encode any non-deterministic Turing machine:

• $x_{q,0}^{7,t}$: at step $t$, the head is a position $7$ in state $q$.
• $r_0^{7,t}$: the position 7 at time $t$ contains a $0$.
• Transitions
  • $\tau_1 = (q,0): (q', 1, \rightarrow)$
  • $\tau_2 = (q,0): (q'', 0, \leftarrow)$
• $(x_{q}^{7,t} \wedge r_0^{7,t}) \Rightarrow$ $(x_{q'}^{8,t+1} \wedge r_1^{7,t+1}) \vee$ $(x_{q''}^{6,t+1} \wedge r_0^{7,t+1})$

NP-completeness

This shows that SAT is NP-complete! (Cook, Levin, 1973)

• For any NP problem (“resonable”), we can write a formula that is SAT if and only if the problem has a solution.
• Most people believes that this cannot be done in polynomial time.
• Why should we try to solve such a hard problem?
  • Efficient algorithms for SAT in practice = efficient algorithm for many other problems
  • Very simple structure: allows for low level optimization.

A Branching algorithm

$$F = (x_1 \vee x_4) \wedge (\neg x_1 \vee \neg x_2) \wedge (x_1 \vee x_3 \vee \neg x_4) \wedge (\neg x_1 \vee x_2 \vee \neg x_4) \wedge (\neg x_1 \vee x_2 \vee x_4) \wedge (x_1 \vee \neg x_2 \vee \neg x_3 \vee x_4)$$

Adding Unit Propagation

$$F = (x_1 \vee x_4) \wedge (\neg x_1 \vee \neg x_2) \wedge (x_1 \vee x_3 \vee \neg x_4) \wedge (\neg x_1 \vee x_2 \vee \neg x_4) \wedge (\neg x_1 \vee x_2 \vee x_4) \wedge (x_1 \vee \neg x_2 \vee \neg x_3 \vee x_4)$$

DPLL

• If every clause are satisfied, return $1$.
• If one clause is refuted, return $0$.

• Otherwise, pick a variable $x$ and $b \in \{0,1\}$ using a good heuristic
• Try to recursively find a solution to $F[x \gets b]$.
• If no solution, backtrack and try $F[x \gets 1-b]$.

CDCL Solvers

Conflict Driven Clause Learning: try to learn why.

• $(x \vee y) \wedge (\neg x \vee u \neg z_1) \wedge (z_1 \vee \neg z_2) \wedge (z_2 \vee \neg y) \vee (z_2 \vee z_1 \vee y)$
• Set $x=1, u=0$: Unit Propagation of $z_1=0, z_2=0, y=0$ : conflict found.
• We know that, independently of the value of $z_1,z_2,y$, $(x=1,u=0)$ cannot be part of a solution.
• Add clause $\neg x \vee u$ to catch it sooner.
  • If we later set $x=1$, we have UP on $u=1$!
  • Speed up later branches.
  • Reduce overhead of recursion.

Counting the number of solutions

• With 1: {1,2}, {1,2,3}, {1,2,3,4}, {1,2,4}, {1,4}, {1,3,4}
• Without 1 and with 2: {2,3,4}
• Without 1,2 and with 3: {3,4}

Why counting?

Modeling constraints: counting enables better “reasoning”.

• Configuration problem:
  • Find some options compatible with a lot of product
  • Measure “probability” of an option (number of product having it)
  • Counting (with weights) = probabilistic reasoning
• Encode other reasoning tasks such as Bayesian inference

How hard is it?

• Counting is way harder than finding a solution
• Intution: we have to explore the entire search space
• Complexity theory: #P-complete problem.
• Toda’s Theorem: one oracle call to #P allows to solve the whole polynomial hierarchy.

Counting by enumeration

$$(x_1 \vee x_3 \vee \neg x_4) \wedge (x_1 \vee x_4) \wedge (\neg x_1 \vee x_2 \vee x_4) \wedge (x_1 \vee \neg x_2 \vee \neg x_3 \vee x_4)$$

Counting by enumeration

$$\#F = \#F[x=0]+\#F[x=1]$$

Caching in Exhaustive DPLL

Exploiting SAT solver efficiency

Exhaustive DPLL for $$F = (\neg x_1 \vee x_2 \vee x_3) \wedge (\neg x_2 \vee \neg x_5) \wedge (x_2 \vee x_4 \vee x_5) \wedge (\neg x_3 \vee \neg x_5) \wedge (x_1) \wedge (\neg x_2 \vee \neg x_4) \wedge (\neg x_3 \vee \neg x_4)$$

Connected components

Observation: $F = F_1 \wedge F_2$ with $var(F_1) \cap var(F_2) = \emptyset$ then

$$\#F = \#F_1 \times \#F_2$$

because solutions of $F_1$ and $F_2$ can be recombined independently to form a solution of $F$.

• Add connected components detection in exhaustive DPLL.
• Reduces the number of operations.

Example with connected components

Exhaustive DPLL: summary

• Run SAT solver to prune unsatisfiable branches. Exploit learnt clauses.
• $\#F = \#F_1 \times \#F_2$ when $F_1$ and $F_2$ have disjoint variables.
• $\#F = \#F[x \gets 0]+\#F[x \gets 1]$ otherwise.
• When $\#G$ is computed, cache its value in case $G$ is encountered again.
• Many tools based on this idea: d4, SharpSAT, SharpSAT-TD, etc.

Choosing variables

• Complexity of exhaustive DPLL depends on the variable picked for branching
• For SAT solver:
  • try to quickly converge to conflicts to learn
  • try to find one solution
  • Many heuristics for this: VSIDS, Bohm, Maximum occurrence etc.
• Very different for #SAT solvers: aim at factorizing the search space.
• Find small separator: treewidth guided heuristics.

Trace of counting algorithm

Syntactic restriction of Boolean circuits

• Trace of exhaustive DPLL: decision-DNNF
• Studied in Knowledge Compilation
• If no decomposable $\wedge$-gate:
  • corresponds to FBDD (Free Binary Decision Diagrams).
  • if static order, OBDD (Ordered Binary Decision Diagrams)

Limits of DPLL

• Long clauses mess with the cache and the decomposition.
• Some natural constraints do not have good encoding into CNF, e.g, PARITY (common in cryptography or circuit synthesis)
• DPLL not appropriate for every constraint problem.

Bottom up compilation

Build a tractable circuit by assembling base tractable circuits:

• $C_1, C_2$ two circuits, build one for $C_1 \wedge C_2$ by combining $C_1$ and $C_2$
• This combination should be doable (depends on the class of circuits).
• Sometimes better: parity constraints have a small tractable circuits representation.

OBDD example