Scoring functions based on second level score for &kappa;-SAT with long clauses

ISCAS OpenIR

	Scoring functions based on second level score for κ-SAT with long clauses
	Cai, Shaowei (1); Luo, Chuan (3); Su, Kaile (4); Cai, Shaowei
	2014
发表期刊	Journal of Artificial Intelligence Research
ISSN	10769757
卷号	51 页码:413-441
摘要	It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models for satisfiable instances of the satisfiability (SAT) problem, especially for random κ-SAT instances. However, compared to random 3-SAT instances where SLS algorithms have shown great success, random κ-SAT instances with long clauses remain very difficult. Recently, the notion of second level score, denoted as score2, was proposed for improving SLS algorithms on long-clause SAT instances, and was first used in the powerful CCASat solver as a tie breaker. In this paper, we propose three new scoring functions based on score2. Despite their simplicity, these functions are very effective for solving random κ-SAT with long clauses. The first function combines score and score2, and the second one additionally integrates the diversification property age. These two functions are used in developing a new SLS algorithm called CScoreSAT. Experimental results on large random 5-SAT and 7-SAT instances near phase transition show that CScoreSAT significantly outperforms previous SLS solvers. However, CScoreSAT cannot rival its competitors on random κ-SAT instances at phase transition. We improve CScoreSAT for such instances by another scoring function which combines score2 with age. The resulting algorithm HScoreSAT exhibits state-of-the-art performance on random κ-SAT (κ > 3) instances at phase transition. We also study the computation of score2, including its implementation and computational complexity.; It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models for satisfiable instances of the satisfiability (SAT) problem, especially for random κ-SAT instances. However, compared to random 3-SAT instances where SLS algorithms have shown great success, random κ-SAT instances with long clauses remain very difficult. Recently, the notion of second level score, denoted as score2, was proposed for improving SLS algorithms on long-clause SAT instances, and was first used in the powerful CCASat solver as a tie breaker. In this paper, we propose three new scoring functions based on score2. Despite their simplicity, these functions are very effective for solving random κ-SAT with long clauses. The first function combines score and score2, and the second one additionally integrates the diversification property age. These two functions are used in developing a new SLS algorithm called CScoreSAT. Experimental results on large random 5-SAT and 7-SAT instances near phase transition show that CScoreSAT significantly outperforms previous SLS solvers. However, CScoreSAT cannot rival its competitors on random κ-SAT instances at phase transition. We improve CScoreSAT for such instances by another scoring function which combines score2 with age. The resulting algorithm HScoreSAT exhibits state-of-the-art performance on random κ-SAT (κ > 3) instances at phase transition. We also study the computation of score2, including its implementation and computational complexity.
收录类别	EI
部门归属	(1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (2) Queensland Research Lab, NICTA, Brisbane, Australia; (3) Key Laboratory of High Confidence Software Technologies, Peking University, Beijing, China; (4) Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/17024
专题	中国科学院软件研究所
通讯作者	Cai, Shaowei
推荐引用方式 GB/T 7714	Cai, Shaowei ,Luo, Chuan ,Su, Kaile ,et al. Scoring functions based on second level score for κ-SAT with long clauses[J]. Journal of Artificial Intelligence Research,2014,51:413-441.
APA	Cai, Shaowei ,Luo, Chuan ,Su, Kaile ,&Cai, Shaowei.(2014).Scoring functions based on second level score for κ-SAT with long clauses.Journal of Artificial Intelligence Research,51,413-441.
MLA	Cai, Shaowei ,et al."Scoring functions based on second level score for κ-SAT with long clauses".Journal of Artificial Intelligence Research 51(2014):413-441.