CCDD: A Tractable Representation for Model Counting and Uniform Sampling
This work addresses the need for tractable operations in knowledge compilation for computer science applications, offering incremental improvements in representation efficiency and query performance.
The paper tackles the problem of efficient model counting and uniform sampling for propositional formulas by introducing a new representation language called CCDD, which introduces restrictions on conjunction nodes to capture equivalent literals, resulting in improved compilation times and solving more instances than prior state-of-the-art methods, with the model counter solving 885 instances (improvement of 43) and the uniform sampler solving 780 instances (improvement of 132).
Knowledge compilation concerns with the compilation of representation languages to target languages supporting a wide range of tractable operations arising from diverse areas of computer science. Tractable target compilation languages are usually achieved by restrictions on the internal nodes of the NNF. In this paper, we propose a new representation language CCDD, which introduces new restrictions on conjunction nodes to capture equivalent literals. We show that CCDD supports two key queries, model counting and uniform samping, in polytime. We present algorithms and a compiler to compile propositional formulas expressed in CNF into CCDD. Experiments over a large set of benchmarks show that our compilation times are better with smaller representation than state-of-art Decision-DNNF, SDD and OBDD[AND] compilers. We apply our techniques to model counting and uniform sampling, and develop model counter and uniform sampler on CNF. Our empirical evaluation demonstrates the following significant improvements: our model counter can solve 885 instances while the prior state of the art solved only 843 instances, representing an improvement of 43 instances; and our uniform sampler can solve 780 instances while the prior state of the art solved only 648 instances, representing an improvement of 132 instances.