3. Boolean Satisfiability Problem

Boolean Satisfiability Problem (SAT)

The Boolean Satisfiability Problem (SAT) takes an input of:

• a propositional formula $F$ in CNF

It provides an output of $\top$ if and only if $F$ is satisfiable.

Link to original

Theorem: SAT problem belongs to NP (upper-bound)

Input: Given some formula $F$ in CNF, we can decide whether $F$ is satisfiable by computing its truth table.

1. However the truth table contains $2^n$ rows which is not polynomial.
2. But, we can use an NDTM to evaluate each row in parallel, now each row requires us to evaluate at most $n$ boolean operators which is polynomial!