Circuit-Aware d-DNNF Compilation

Abstract

Boolean circuits in d-DNNF (determinstic Decomposable Negation Normal Form) enable tractable probabilistic inference, motivating research into compilers that transform arbitrary Boolean circuit into this form. However, d-DNNF compilers commonly require the input to be in conjunctive normal form (CNF), which means that a user must first convert their Boolean circuit into CNF. In this work, we argue that d-DNNF compilation would substantially benefit from reasoning over the original input circuit's structure, rather than solely relying on its CNF representation. To this end, we adapt an existing compiler and implement an optimisation that becomes more readily available once we reason over the input circuit: the identification and elimination of don't care variables. We empirically demonstrate the effectiveness of this approach, achieving a significant improvement in both the number of solved instances and the size of the resulting circuits.