arXiv 2005.040222020-05-07cs.AIcs.LO

学习子句对随机局部搜索的影响

On the Effect of Learned Clauses on Stochastic Local Search

Ulm University（乌尔姆大学）

Jan-Hendrik Lorenz, Florian Wörz

备注：: Accepted at 'The 23rd International Conference on Theory and Applications of Satisfiability Testing'

摘要：

在成功的SAT求解器中有两种相互竞争的范式：随机驱动的子句学习（CDCL）和随机局部搜索（SLS）。CDCL系统地探索搜索空间，并具有学习新子句的能力。SLS检查当前完整分配的邻域。与CDCL不同，它缺乏从错误中学习的能力。这项工作围绕着SLS在原始公式中添加新条款是否有益的问题展开。我们的实验表明，条款与大量的正确文字w。R. t.一个固定的解决方案是有益的运行SLS。我们称这种条款为高质量条款。实验结果表明，CDCL学习的短句具有高质量的属性。我们研究了几个领域的随机生成的实例，并推导出最有益的策略，添加高质量的条款作为预处理步骤。在SLS求解器中实现的策略，它表明，这大大提高了国家的最先进的随机生成的实例。结果具有统计学意义。

英文摘要：

There are two competing paradigms in successful SAT solvers: Conflict-driven clause learning (CDCL) and stochastic local search (SLS). CDCL uses systematic exploration of the search space and has the ability to learn new clauses. SLS examines the neighborhood of the current complete assignment. Unlike CDCL, it lacks the ability to learn from its mistakes. This work revolves around the question whether it is beneficial for SLS to add new clauses to the original formula. We experimentally demonstrate that clauses with a large number of correct literals w. r. t. a fixed solution are beneficial to the runtime of SLS. We call such clauses high-quality clauses. Empirical evaluations show that short clauses learned by CDCL possess the high-quality attribute. We study several domains of randomly generated instances and deduce the most beneficial strategies to add high-quality clauses as a preprocessing step. The strategies are implemented in an SLS solver, and it is shown that this considerably improves the state-of-the-art on randomly generated instances. The results are statistically significant.

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

摘要：

英文摘要：

相关论文