Tags:knowledge compilation, model counting and uniform sampling
Abstract:
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 ($\land$ or $\lor$) of the NNF. Recently, a new representation language CCDD, which introduces new restrictions on conjunction nodes to capture equivalent literals, was proposed. We show that CCDDsupports uniform sampling 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 representations than state-of-art Decision-DNNF, SDD and OBDDC[AND] compilers. We apply our techniques to uniform sampling, and develop a uniform sampler on CNF. Our empirical evaluation demonstrates that our uniform sampler can solve 780 instances while the prior state of the art solved only 648 instances, representing a significant improvement of 132 instances.
Scalable Uniform Sampling via Efficient Knowledge Compilation