Satisfiability Problem

computation

Definition

Satisfiability Problem

The SAT problem is a decision problem that, for a given Boolean function $\Phi (\mathbf{x})$, checks whether there exists a variable assignment ${\mathbf{x}}_0$ of true and false values such that $\Phi ({\mathbf{x}}_0)$.

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.