Skip to main content

3SAT is a famous special case of the boolean satisfiability problem (SAT).

3SAT (3CNF satisfiability) is a particular case of boolean satisfiability problem. It restricts the space of considered formulae to those in 3CNF, that is formulae in conjunctive normal form with at most three literals per clause, e.g. \[(a\lor b) \land (b \lor c \lor d) \land d\]

3SAT is an NP-complete problem and is often used as basis of reduction proofs in complexity theory.