arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 0910.1244cs.AI
收藏

关于改进的局部不可满足性搜索

On Improving Local Search for Unsatisfiability

IST/INESC-ID(里斯本高等技术学院/葡萄牙国家系统与计算机工程研究所-ID分院);Technical University of Lisbon(里斯本技术大学);Cork Constraint Computation Centre(科克约束计算中心)

David Pereira, Inês Lynce, Steven Prestwich

摘要:

随机局部搜索(SLS)在过去的几年里一直是一个活跃的研究领域,新的技术和程序正在以惊人的速度发展。SLS传统上与可满足性求解相关联,即为给定的问题实例找到解决方案,因为其内在本质并不解决不可满足的问题。因此,通常使用回溯搜索求解器来解决不可满足的实例。出于这个原因,在90年代后期,Selman,Kautz和McAllester提出了一个挑战,使用局部搜索来证明不可满足性。最近,两个SLS解算器- Ranger和Gunsat -已经开发出来,尽管是SLS解算器,但它们能够证明不可满足性。在本文中,我们首先比较游侠与Gunsat,然后提出提高游侠的性能,使用Gunsat的一些技术,即单位传播前瞻和扩展分辨率。

英文摘要:

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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑