Satisfiability Problem

SAT and UNSAT Problems


Boolean satisfiability problem (SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula which is involving conjunction (AND, ), disjunction (OR, ) and negation (NOT, ). SAT is the first problem that was proven to be NP-complete.

For simplicity, it is common to require that the boolean expression be written in conjunction normal form or "CNF". A formula in conjunctive normal form consists:

  1. clauses joined by AND;
  2. each clause, in turn, consists of literals joined by OR;
  3. each literal is either the name of a variable (a positive literal), or the name of a variable preceded by NOT (a negative literal).

An example of a boolean expression in 3 variables and 2 clauses:

(x1¬x3)(¬x1x2x3)(x_{1}\vee \neg x_{3}) \wedge (\neg x_{1} \vee x_{2} \vee x_{3})

In this example, SAT problem needs to find an assignment of , for instance , to make the formula true.


UNSAT is the opposite of the SAT task, which requires proving that there is no assignment method that makes a Boolean formula true.

Last Updated: 01/04/2022