论文标题
CCDD：用于模型计数和均匀抽样的可拖动表示
CCDD: A Tractable Representation for Model Counting and Uniform Sampling
论文作者
论文摘要
知识汇编涉及代表性语言汇编的目标语言，这些语言支持由计算机科学的各个领域引起的广泛可进行操作。通常通过对NNF内部节点的限制来实现可进行的目标编译语言。在本文中，我们提出了一种新的表示语言CCDD，该语言介绍了对连词节点的新限制以捕获等效的文字。我们表明，CCDD支持两个关键查询，即模型计数和均匀的samping，以多态时间。我们提出算法和编译器，以编译CNF中表达为CCDD的命题公式。大量基准测试的实验表明，我们的编译时间比最先进的决策-DNNF，SDD和OBDD [and]编译器更好。我们将技术应用于模型计数和均匀的采样，并在CNF上开发模型计数器和均匀采样器。我们的经验评估证明了以下重大改进：我们的模型计数器可以解决885个实例，而先前的最新情况仅解决了843个实例，代表了43个实例；而且我们的统一采样器可以解决780个实例，而先前的最新情况仅解决了648个实例，代表了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.
