小句学习潜力的理解和利用
Towards Understanding and Harnessing the Potential of Clause Learning
摘要：
添加子句学习的DPLL的有效实现是最快的完整布尔可满足性求解器，并且可以处理许多重要的现实问题，例如验证，规划和设计。尽管它很重要，但人们对这项技术的最终优势和局限性知之甚少。本文提出了第一个精确的表征小句学习作为一个证明系统（CL），并开始了解它的权力，将其与研究充分的决议证明系统的任务。特别是，我们表明，与一个新的学习计划，CL可以提供指数更短的证明比许多适当的改进一般决议（RES）满足自然属性。这些包括常规和Davis-Putnam分辨率，已知其比普通DPLL强得多。我们还表明，CL的一个轻微的变化与无限的重新启动是一样强大的RES本身。然而，由于子句学习算法的不确定性，将这些分析结果转化为实践提出了挑战。我们提出了一种新的方式，利用底层的问题结构，在一个高层次的问题描述，如图或PDDL规范的形式，引导条款学习算法更快的解决方案。我们表明，这导致指数加速网格和随机卵石问题，以及某些排序公式的实质性改进。
英文摘要：
Efficient implementations of DPLL with the addition of clause learning are the fastest complete Boolean satisfiability solvers and can handle many significant real-world problems, such as verification, planning and design. Despite its importance, little is known of the ultimate strengths and limitations of the technique. This paper presents the first precise characterization of clause learning as a proof system (CL), and begins the task of understanding its power by relating it to the well-studied resolution proof system. In particular, we show that with a new learning scheme, CL can provide exponentially shorter proofs than many proper refinements of general resolution (RES) satisfying a natural property. These include regular and Davis-Putnam resolution, which are already known to be much stronger than ordinary DPLL. We also show that a slight variant of CL with unlimited restarts is as powerful as RES itself. Translating these analytical results to practice, however, presents a challenge because of the nondeterministic nature of clause learning algorithms. We propose a novel way of exploiting the underlying problem structure, in the form of a high level problem description such as a graph or PDDL specification, to guide clause learning algorithms toward faster solutions. We show that this leads to exponential speed-ups on grid and randomized pebbling problems, as well as substantial improvements on certain ordering formulas.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
