Translating propositional logic to Datalog (ctd)
(p ∨ ¬q ∨ r) ∧
(p ∨ ¬q ∨ ¬r) ∧
(p ∨ q ∨ r)
A clause holds if any literal is true, so it gets one rule per literal; sat needs all clauses at once:
The query returns all 5 satisfying assignments of the formula.