Tseitin transformation from a boolean Crux.Expression into CNF.
The naive distributive-law CNF conversion can blow up exponentially
((a₁ AND b₁) OR ... OR (aₙ AND bₙ) produces 2ⁿ clauses). Tseitin
introduces a fresh auxiliary variable for each compound subexpression
and emits clauses that bind the auxiliary to the subexpression's truth
value. The resulting CNF grows linearly in the size of the expression
at the cost of those auxiliary variables.
The transformation preserves satisfiability and — because the encoding
is the full biconditional (x ↔ subexpr) — every user-variable
assignment uniquely determines the auxiliary variables, so the set of
satisfying user-variable models is identical to the original
expression's.
Summary
Functions
Tseitin-encodes expression into CNF.
Functions
@spec transform(Crux.Expression.t(variable)) :: Crux.Formula.t(variable) when variable: term()
Tseitin-encodes expression into CNF.
Assumes expression is neither the literal true nor false —
callers should short-circuit those at a higher level. Booleans nested
inside the expression are handled.
The returned Formula separates the auxiliary definition clauses
(:definitions) from the full CNF (:cnf). Consumers that want to
negate the formula (for implication tests) must keep the definition
clauses required; auxiliaries are not freely assignable. :bindings
and :reverse_bindings only cover user-supplied variables, never
auxiliaries; the auxiliary ids live in :auxiliaries.