Given a CNF formula, kompyle compiles it into a d-DNNF circuit.
It is important that kompyle indeed constructs the circuit that is
the same Boolean function as the CNF formula.
At the moment, this is checked by only exhaustively checking all assignments for somewhat
smaller formulas, which is infeasible for practical CNF files.
It would be useful to support a scalable method to verify equivalence between larger
CNF formulas and its compiled d-DNNF representations without exhaustive enumeration.
No need for a proof, but for checking individual instances
Given a CNF formula,
kompylecompiles it into a d-DNNF circuit.It is important that
kompyleindeed constructs the circuit that isthe same Boolean function as the CNF formula.
At the moment, this is checked by only exhaustively checking all assignments for somewhat
smaller formulas, which is infeasible for practical CNF files.
It would be useful to support a scalable method to verify equivalence between larger
CNF formulas and its compiled d-DNNF representations without exhaustive enumeration.
No need for a proof, but for checking individual instances