Translating propositional logic to Datalog

To find a formula's satisfying assignments, enumerate all assignments and keep those that satisfy it.

By safety, a comparison can only test already-bound variables, so we first generate every assignment (binding P, Q, R), then let the clauses test them.