Conflict-driven clause learning

The satisfiability problem consists in finding a satisfying assignment for a given formula in conjunctive normal form (CNF).

An example of such a formula is:

( (not A) or (not C) )   and   (B or C),

or, using a common notation:[4]

${\displaystyle (\lnot A\lor \lnot C)\land (B\lor C)}$

where A,B,C are Boolean variables, ${\displaystyle \lnot A}$, ${\displaystyle \lnot C}$, ${\displaystyle B}$, and ${\displaystyle C}$ are literals, and ${\displaystyle \lnot A\lor \lnot C}$ and ${\displaystyle B\lor C}$ are clauses.

A satisfying assignment for this formula is e.g.:

${\displaystyle A=\mathrm {False} ,B=\mathrm {False} ,C=\mathrm {True} }$

since it makes the first clause true (since ${\displaystyle \lnot A}$ is true) as well as the second one (since ${\displaystyle C}$ is true).

This examples uses three variables (A, B, C), and there are two possible assignments (True and False) for each of them. So one has ${\displaystyle 2^{3}=8}$ possibilities. In this small example, one can use brute-force search to try all possible assignments and check if they satisfy the formula. But in realistic applications with millions of variables and clauses brute force search is impractical. The responsibility of a SAT solver is to find a satisfying assignment efficiently and quickly by applying different heuristics for complex CNF formulas.

If an unsatisfied clause has all but one of its literals or variables evaluated at False, then the free literal must be True in order for the clause to be True. For example, if the below unsatisfied clause is evaluated with ${\displaystyle A=\mathrm {False} }$ and ${\displaystyle B=\mathrm {False} }$ we must have ${\displaystyle C=\mathrm {True} }$ in order for the clause ${\displaystyle (A\lor B\lor C)}$ to be true.

The iterated application of the unit clause rule is referred to as unit propagation or Boolean constraint propagation (BCP).

Consider two clauses ${\displaystyle (A\lor B\lor C)}$ and ${\displaystyle (\neg C\lor D\lor \neg E)}$. The clause ${\displaystyle (A\lor B\lor D\lor \neg E)}$, obtained by merging the two clauses and removing both ${\displaystyle \neg C}$ and ${\displaystyle C}$, is called the resolvent of the two clauses.