Satisfiability. We turn now to one of the most fundamental problems of computer science: Given a Boolean Formula $F(x_1,…,x_n)$, expressed in so-called “conjunctive normal form” as an AND of ORs, can we “satisfy” $F$ by assigning values to its variables in such a way that $F(x_1,…,x_2) = 1$?

Note: Change math to MathML… and finish proper citation

[0] Knuth 7.2.2.2 TAOCP