Chapter 7. Combinatorial Searching

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)

7.2.2.2. Satisfiability

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

Image

is satisfied when x1x2x3 = 001. But if we rule that solution out, by defining ...

Get The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6 now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.

Start your free trial