A propositional logic interpreter
One fixed set of rules solves any CNF. No separate predicate per clause is needed:
A clause is satisfied when one of its literals is true (its variable's value matches the polarity, via
lookup).
An assignment falsifies the formula if some clause is left unsatisfied.
satisfies yields 0b001, 0b011, 0b100, 0b101, 0b111.