He reaps no satisfaction but from low and sensual objects,or from the indulgence of malignant passions.
— DAVID HUME, The Sceptic (1742)
I can’t get no . . .
— MICK JAGGER and KEITH RICHARDS, Satisfaction (1965)
We turn now to one of the most fundamental problems of computer science: Given a Boolean formula F (x1, . . . , xn), 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 (x1, . . . , xn) = 1? For example, the formula
is satisfied when x1x2x3 = 001. But if we rule that solution out, by defining ...