# 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**, **OR**, **NOT**,

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:

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

## UNSAT

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