Satisfiability Problem

SAT and UNSAT Problems

SAT

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:

$(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

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