Local search for Boolean Satisfiability with configuration checking and   subscore

doi:10.1016/j.artint.2013.09.001

CORC > 北京大学 > 信息科学技术学院

	Local search for Boolean Satisfiability with configuration checking and subscore
	Cai, Shaowei ; Su, Kaile
刊名	人工智能
	2013
关键词	SAT Local search Configuration checking Subscore MINIMUM VERTEX COVER TABU SEARCH K-SAT ALGORITHM EXPRESSIONS
DOI	10.1016/j.artint.2013.09.001
英文摘要	This paper presents and analyzes two new efficient local search strategies for the Boolean Satisfiability (SAT) problem. We start by proposing a local search strategy called configuration checking (CC) for SAT. The CC strategy results in a simple local search algorithm for SAT called Swcc, which shows promising experimental results on random 3-SAT instances, and outperforms TNM, the winner of SAT Competition 2009. However, the CC strategy for SAT is still in a nascent stage, and Swcc cannot yet compete with Sparrow2011, which won SAT Competition 2011 just after Swcc had been designed. The CC strategy seems too strict in that it forbids flipping those variables even with great scores, if they do not satisfy the CC criterion. We improve the CC strategy by adopting an aspiration mechanism, and get a new variable selection heuristic called configuration checking with aspiration (CCA). The CCA heuristic leads to an improved algorithm called Swcca, which exhibits state-of-the-art performance on random 3-SAT instances and crafted ones. The third contribution concerns improving local search algorithms for random k-SAT instances with k>3. Although the SAT community has made great achievements in solving random 3-SAT instances, the progress lags far behind on random k-SAT instances with k>3. This work proposes a new variable property called subscore, which is utilized to break ties in the CCA heuristic when candidate variables for flipping have the same score. The resulting algorithm CCAsubscore is very efficient for solving random k-SAT instances with k>3, and significantly outperforms other state-of-the-art ones. Combining Swcca and CCAsubscore, we obtain a local search SAT solver called CCASat, which was ranked first in the random track of SAT Challenge 2012. Additionally, we perform theoretical analyses on the CC strategy and the subscore property, and show interesting results on these two heuristics. Particularly, our analysis indicates that the CC strategy is more effective for k-SAT with smaller k, while the subscore notion is not suitable for solving random 3-SAT. (C) 2013 Elsevier B.V. All rights reserved.; Computer Science, Artificial Intelligence; SCI(E); EI; 7; ARTICLE; 75-98; 204
语种	英语
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/224066]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	Cai, Shaowei,Su, Kaile. Local search for Boolean Satisfiability with configuration checking and subscore[J]. 人工智能,2013.
APA	Cai, Shaowei,&Su, Kaile.(2013).Local search for Boolean Satisfiability with configuration checking and subscore.人工智能.
MLA	Cai, Shaowei,et al."Local search for Boolean Satisfiability with configuration checking and subscore".人工智能 (2013).