Closes the deduction leg: propositional formula strings (as emitted by
meaning_graph.to_deductive_logic, or any logic_canonical-parseable syntax) →
corridor CNF PropositionalProblem + query Clause, consumable by
propositional_entails.
Structural, not truth-table (spike §4.1): reuses the production ROBDD parser
(generate.logic_canonical — never re-implemented) for the AST, then the standard
sound rewrite — eliminate iff/implies, NNF, distribute OR over AND — with
constant folding, tautological-clause elimination, and a clause budget. The
converter never enumerates assignments and never decides entailment; that stays
the corridor's job.
Soundness proved against the ROBDD oracle: for a 14-formula panel, the compiled
CNF rendered back to a formula has the same canonicalize() identity as the
source. End-to-end entailment through propositional_entails agrees with the
ROBDD gold (evaluate_entailment) wrong=0 on consistent premises; ex-falso
handled per the corridor's own contract (entailed + satisfiable_premises=False,
where the ROBDD path returns REFUSED for inconsistent premises).
Fail-closed: conjunctive/constant queries, formulas reducing to false, and CNF
budget refuse with typed CnfCompileError; >5 atoms surfaces the corridor's
HamiltonianCompileError(atom_count_out_of_range); out-of-regime propagates
LogicRegimeError. Off-serving (A-04), import-guard pinned.
32/32 pins green.
[Verification]: uv run python -m pytest tests/test_adr_0249_logic_cnf_compiler.py -q
