理解与利用子句学习潜力的探索
人工智能
2011-07-04 v1
摘要
带有子句学习的DPLL高效实现是最快的完备布尔可满足性求解器，能够处理许多重要的现实世界问题，如验证、规划和设计。尽管其重要性不言而喻，但人们对这项技术的最终优势与局限知之甚少。本文首次将子句学习精确刻画为一个证明系统（CL），并通过将其与得到深入研究的归结证明系统相关联，开始理解其能力。特别地，我们证明，通过一种新的学习策略，CL可以提供比满足某一自然性质的通用归结（RES）的许多适当精化指数级更短的证明。这些精化包括正则归结和Davis-Putnam归结，已知它们比普通DPLL强得多。我们还证明，带有无限重启的CL的一个轻微变体与RES本身一样强大。然而，由于子句学习算法的非确定性本质，将这些分析结果转化为实践面临挑战。我们提出了一种利用底层问题结构的新方法，以高层问题描述（如图或PDDL规约）的形式，来引导子句学习算法更快地求解。我们证明，这在网格和随机堆石问题上带来了指数级加速，并在某些排序公式上取得了显著改进。
引用
@article{arxiv.1107.0044,
title = {Towards Understanding and Harnessing the Potential of Clause Learning},
author = {P. Beame and H. Kautz and A. Sabharwal},
journal= {arXiv preprint arXiv:1107.0044},
year = {2011}
}