On Compiling DNNFs without Determinism
  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.
