Satisfiability Problem

computation

Definition

Satisfiability Problem

The SAT problem is a decision problem that, for a given formula $\Phi$, checks whether there exists a interpretation $v$ such that $v(\Phi )=1$.

Tractable Classes

Horn Formulas

Solving Horn formulas is a tractable problem.

Krom Formula

Solving Krom formulas is a tractable problem.

Reductions

Reduction to CSP

The SAT problem can be reduced to a constraint satisfaction problem by translating Boolean variables into CSP variables and clauses into constraints.

Variables: Let $\Phi$ be a Boolean formula with variables $x_1,\dots ,x_n$. The CSP instance uses exactly these variables as its variable set $V=\{x_1,\dots ,x_n\}$.

Domain: Each variable ranges over the domain $D=\{0,1\}$, where $0$ represents $\perp$ and $1$ represents $\top$.

Constraints: For every clause $C=({\ell }_1\vee \cdots \vee {\ell }_r)$ of $\Phi$, add one constraint whose scope consists of the variables occurring in $C$. Its relation contains exactly those tuples in $\{0,1{\}}^r$ that satisfy the clause. Hence the only excluded tuples are those that make all literals in the clause false.

Encoding a Clause as a Constraint

The clause

$$(x\vee y\vee \neg z)$$

is encoded by a ternary constraint on $(x,y,z)$ whose relation is

$$R=\{(1,0,1),(0,1,1),(1,1,1),(0,0,0),(1,0,0),(0,1,0),(1,1,0)\}.$$

The only forbidden tuple is $(0,0,1)$, since it is the unique assignment for which $x=\perp$, $y=\perp$, and $z=\top$, making $\neg z=\perp$ as well.

Correctness: A Boolean assignment satisfies $\Phi$ if and only if the corresponding CSP assignment satisfies every constraint. Therefore the constructed CSP instance is satisfiable exactly when the original SAT instance is satisfiable.

Example

Logic Olympiad Puzzle

There were three finalists: Louis, Rene, and Johannes.

We use Boolean variables $L_1,\dots ,J_3$ to denote a person and their placing.

person	1	2	3
Louis	$L_1$	$L_2$	$L_3$
Rene	$R_1$	$R_2$	$R_3$
Johannes	$J_1$	$J_2$	$J_3$

Isaac reported that Louis won the olympiad, while Rene was second:

$(L_1\wedge R_2)$

Albert reported that Johannes won the olympiad, while Louis was second:

$(J_1\wedge L_2)$

Neither report was completely correct, and each report had one true and one false statement:

$(\neg L_1\vee \neg R_2)(\neg J_1\vee \neg L_2)$

The hidden constraints are that exactly one contestant is first, exactly one is second, exactly one is third, and each contestant takes exactly one place. This yields a SAT instance with a unique model:

$(L_1=0,L_2=0,L_3=1,R_1=0,R_2=1,R_3=0,J_1=1,J_2=0,J_3=0)$

Hence, Johannes won, Rene was second, and Louis came third.

Unit Propagation

Definition

Unit Propagation

Let $S$ be a set of clauses. Unit propagation is the repeated application of the following transformation.

If $S$ contains a unit clause, that is, a clause consisting of a single literal $L$, then:

1. Remove from $S$ every clause of the form $L\vee C$.
2. Replace in $S$ every clause of the form $\neg L\vee C$ by the clause $C$.

The process continues until no unit clause remains. At that point one of three situations holds:

• $S$ is empty: every clause was satisfied, so the original set is satisfiable.
• $S$ contains the empty clause $\square$: a contradiction was derived, so the original set is unsatisfiable.
• $S$ contains non-unit clauses only: no further simplification is possible without choosing a literal to branch on.

Intuitively, $L$ must be true, so every clause containing $L$ is already satisfied and can be discarded, while $\neg L$ is false and can be deleted from every clause that contains it.

Link to original