论文标题
关于学习条款对随机本地搜索的影响
On the Effect of Learned Clauses on Stochastic Local Search
论文作者
论文摘要
成功的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.
