Satisfying and falsifying assignments

The root’s value decides everything:

satisfies(A)  :- root(R), eval(R, A, 1).
satisfiable() :- satisfies(_).

falsifies(A)  :- root(R), eval(R, A, 0).
valid()       :- not falsifies(_).

For (¬(p ∨ q) ∧ r) ∨ p, satisfies returns the same five assignments as Part 1’s CNF solver: 0b001, 0b011, 0b100, 0b101, 0b111. No CNF needed.
A valid formula like ((p → q) → p) → p has no counterexample, so valid is yes.

One machine, any formula. Recursion over the tree did the same work that flattening to CNF did before, but for formulas of every shape.