On Compiling DNNFs without Determinism
This addresses a bottleneck in knowledge compilation for AI and logic, offering potential efficiency gains, though it appears incremental as it builds on existing techniques with auxiliary variables.
The paper tackles the problem that deterministic DNNFs are exponentially less succinct than general DNNFs, proposing a method to compile DNNFs without enforcing determinism, which theoretically can generate exponentially smaller DNNFs and empirically advances compilation on certain benchmarks.
State-of-the-art knowledge compilers generate deterministic subsets of DNNF, which have been recently shown to be exponentially less succinct than DNNF. In this paper, we propose a new method to compile DNNFs without enforcing determinism necessarily. Our approach is based on compiling deterministic DNNFs with the addition of auxiliary variables to the input formula. These variables are then existentially quantified from the deterministic structure in linear time, which would lead to a DNNF that is equivalent to the input formula and not necessarily deterministic. On the theoretical side, we show that the new method could generate exponentially smaller DNNFs than deterministic ones, even by adding a single auxiliary variable. Further, we show that various existing techniques that introduce auxiliary variables to the input formulas can be employed in our framework. On the practical side, we empirically demonstrate that our new method can significantly advance DNNF compilation on certain benchmarks.