Knowledge compilation refers to translating a data structure into another one to enable better algorithmic properties for specific tasks. For instance, model counting (#SAT) and uniform random sampling are likely to be not efficiently solvable for formulas in conjunctive normal form (CNF). However, compiling a CNF into deterministic decompositional negation normal form (d-DNNF) enables an efficient solution. Compilation into reduced ordered binary decision diagrams (BDDs) further admits efficient equivalence checking. Obviously, the complexity of solving hard reasoning tasks thus shifts to the knowledge compilation process.
In this talk I will discuss recent advancements and ongoing work to improve the performance of BDD knowledge compilation. This includes techniques such as SAT preprocessing, variable and clause ordering heuristics, and BDD approximations.