Improving configuration checking for satisfiable random k-SAT instances

详细信息    查看全文

• 作者：André Abramé ; Djamal Habet…
• 关键词：Local search ; Configuration checking ; Novelty heuristic ; Random k ; SAT
• 刊名：Annals of Mathematics and Artificial Intelligence
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：79
• 期：1-3
• 页码：5-24
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence (incl. Robotics); Mathematics, general; Computer Science, general; Complex Systems;
• 出版者：Springer International Publishing
• ISSN：1573-7470
• 卷排序：79

文摘

Local search algorithms based on the Configuration Checking (CC) strategy have been shown to be efficient in solving satisfiable random k-SAT instances. The purpose of the CC strategy is to avoid the cycling problem, which corresponds to revisiting already flipped variables too soon. It is done by considering the neighborhood of the formula variables. In this paper, we propose to improve the CC strategy on the basis of an empirical study of a powerful algorithm using this strategy. The first improvement introduces a new and simple criterion, which refines the selection of the variables to flip for the 3-SAT instances. The second improvement is achieved by using the powerful local search algorithm Novelty with the adaptive noise setting. This algorithm enhances the efficiency of the intensification and diversification phases when solving k-SAT instances with k ≥ 4. We name the resulting local search algorithm Ncca+ and show its effectiveness when treating satisfiable random k-SAT instances issued from the SAT Challenge 2012. Ncca+ won the bronze medal of the random SAT track of the SAT Competition 2013.