Problem. SAT [SAT]

SAT is the canonical problem in NP (like how ATMA_{\text{TM}} was our canonical undecidable problem).

SAT={⟨φ⟩:φis a Boolean formula for which there exists a satisfying truth assignment}\text{SAT} = \left\{ {\left\langle \varphi \right\rangle:\varphi\ \text{is a Boolean formula for which there exists a satisfying truth assignment}} \right\}

  • e.g. φ(x1,x2,x3,x4,x5)=(((x1∨x2)∧(x1∨¬x3∨x4))∨¬(x2∧x3)∨x4)∧¬x5\varphi\left( {x_{1},x_{2},x_{3},x_{4},x_{5}} \right) = \left( {\left( {\left( {x_{1} \vee x_{2}} \right) \land \left( {x_{1} \vee \neg x_{3} \vee x_{4}} \right)} \right) \vee \neg\left( {x_{2} \land x_{3}} \right) \vee x_{4}} \right) \land \neg x_{5}

    • helpful to visualize with a tree diagram

A satisfying truth assignment is an assignment of true/false to each variable so that the whole formula is true.

Problem. 3SAT [3SAT]

Definition 1. Conjunctive Normal Form [cnf]

A problem is in conjunctive normal form (CNF) if it is a product of sums: i.e. an AND of ORs.

Example. 3SAT\text{3SAT}

3SAT={⟨φ⟩:φis a Boolean formula in CNF with 3 literals per clause for which there exists a satisfying truth assignment}\text{3SAT} = \left\{ {\left\langle \varphi \right\rangle:\varphi\ \text{is a Boolean formula in CNF with 3 literals per clause for which there exists a satisfying truth assignment}} \right\}

  • e.g. (x1∨¬x2∨x3)∧(x5∨x4∨¬x2)∧(¬x4∨x1∨x3)∧(¬x3∨x2∧¬x1)\left( {x_{1} \vee \neg x_{2} \vee x_{3}} \right) \land \left( {x_{5} \vee x_{4} \vee \neg x_{2}} \right) \land \left( {\neg x_{4} \vee x_{1} \vee x_{3}} \right) \land \left( {\neg x_{3} \vee x_{2} \land \neg x_{1}} \right)