CCDD：一种易于处理的模型计数和均匀采样表示
CCDD: A Tractable Representation for Model Counting and Uniform Sampling
摘要：
知识编译涉及将表示语言编译为目标语言，以支持来自计算机科学的不同领域的各种易于处理的操作。易处理的目标编译语言通常通过对NNF内部节点的限制来实现。在本文中，我们提出了一个新的表示语言CCDD，它引入了新的限制合取节点捕捉等价的文字。我们表明，CCDD支持两个关键的查询，模型计数和统一采样，在多时间。我们提出的算法和编译器编译CNF到CCDD表示的命题公式。在大量基准测试中的实验表明，我们的编译时间比最先进的Decision-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
