摘要翻译:
随机局部搜索(SLS)是近几年来一个活跃的研究领域,新的技术和方法以惊人的速度发展。SLS传统上与可满足性求解联系在一起,即为给定的问题实例找到一个解决方案,因为它的本质不解决不可满足的问题。因此,不能满足的实例通常使用回溯搜索求解器来解决。出于这个原因,在90年代末,塞尔曼、考茨和麦卡莱斯特提出了一个挑战,即使用本地搜索来证明不可满足性。最近,开发了两个SLS求解器--Ranger和Gunsat,尽管它们是SLS求解器,但它们能够证明不可满足。本文首先对Ranger和Gunsat进行了比较,然后提出了利用Gunsat的一些技术来提高Ranger的性能,即单位传播超前和扩展分辨率。
---
英文标题:
《On Improving Local Search for Unsatisfiability》
---
作者:
David Pereira, In\^es Lynce, Steven Prestwich
---
最新提交年份:
2009
---
分类信息:
一级分类:Computer Science 计算机科学
二级分类:Artificial Intelligence
人工智能
分类描述:Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域,除了视觉、机器人、机器学习、多智能体系统以及计算和语言(自然语言处理),这些领域有独立的学科领域。特别地,包括专家系统,定理证明(尽管这可能与计算机科学中的逻辑重叠),知识表示,规划,和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
---
英文摘要:
Stochastic local search (SLS) has been an active field of research in the last few years, with new techniques and procedures being developed at an astonishing rate. SLS has been traditionally associated with satisfiability solving, that is, finding a solution for a given problem instance, as its intrinsic nature does not address unsatisfiable problems. Unsatisfiable instances were therefore commonly solved using backtrack search solvers. For this reason, in the late 90s Selman, Kautz and McAllester proposed a challenge to use local search instead to prove unsatisfiability. More recently, two SLS solvers - Ranger and Gunsat - have been developed, which are able to prove unsatisfiability albeit being SLS solvers. In this paper, we first compare Ranger with Gunsat and then propose to improve Ranger performance using some of Gunsat's techniques, namely unit propagation look-ahead and extended resolution.
---
PDF链接:
https://arxiv.org/pdf/0910.1244