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,
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:
- clauses joined by AND;
- each clause, in turn, consists of literals joined by OR;
- 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:
In this example, SAT problem needs to find an assignment of
UNSAT is the opposite of the SAT task, which requires proving that there is no assignment method that makes a Boolean formula true.