CNF SAT problem

Problem

A Conjunctive Normal Form Boolean Satisfiability problem is a Boolean Satisfiability problem where all the clauses in $L$ all take the form

$\bigvee_{i=1}^n v_i$

where $v_i$ is either a single variable or a the negation of a single variable.

Example

$x_1 \lor x_2$

$\neg x_1$

$x_1 \lor \neg x_2 \lor \neg x_3 \lor x_4 \lor x_5 \lor \neg x_6 \lor x_7$

are all in conjunctive normal form.

$x_1 \implies x_2$

$\neg (x_1 \lor x_2)$

$x_1 \land x_2$

are not in conjunctive normal form.

See Also

CNF SAT is NP-complete.