论文标题
知识汇编中的相变行为
Phase Transition Behavior in Knowledge Compilation
论文作者
论文摘要
SAT中的相变行为的研究导致了对现代SAT求解器的更深入的了解和算法的改进。在SAT中对相位过渡的这些先前的研究中，我们试图在知识汇编的背景下研究随机K-CNF公式的大小和编译时间行为的行为。 我们对不同知识汇编形式（及其相应的汇编算法）的大小和运行时行为进行了严格的经验研究，并进行了分析：跨多种工具和汇编算法的D-DNNF，SDD和OBDD。我们采用从随机K-CNF模型产生的具有不同生成参数的实例，从经验上讲这些语言的大小和编译时间的中位行为和中位行为。我们的工作在精神上与CSP社区中关于SAT/CSP中相过渡行为的早期工作相似。本着类似的精神，我们确定了相对于不同参数的有趣行为：子句密度和溶液密度，这是一种新的控制参数，我们为研究知识汇编而言研究相变行为。此外，我们用两种具体猜想来总结我们的经验研究。对这些猜想的严格研究可能需要新的理论工具。
The study of phase transition behaviour in SAT has led to deeper understanding and algorithmic improvements of modern SAT solvers. Motivated by these prior studies of phase transitions in SAT, we seek to study the behaviour of size and compile-time behaviour for random k-CNF formulas in the context of knowledge compilation. We perform a rigorous empirical study and analysis of the size and runtime behavior for different knowledge compilation forms (and their corresponding compilation algorithms): d-DNNFs, SDDs and OBDDs across multiple tools and compilation algorithms. We employ instances generated from the random k-CNF model with varying generation parameters to empirically reason about the expected and median behavior of size and compilation-time for these languages. Our work is similar in spirit to the early work in CSP community on phase transition behavior in SAT/CSP. In a similar spirit, we identify the interesting behavior with respect to different parameters: clause density and solution density, a novel control parameter that we identify for the study of phase transition behavior in the context of knowledge compilation. Furthermore, we summarize our empirical study in terms of two concrete conjectures; a rigorous study of these conjectures will possibly require new theoretical tools.
