|
| 作者 | Cai, Shaowei (1)
; Luo, Chuan (3)
; Su, Kaile (4)
|
| 刊名 | Journal of Artificial Intelligence Research
 |
| 出版日期 | 2014
|
| 卷号 | 51页码:413-441 |
| ISSN号 | 10769757
|
| 通讯作者 | Cai, Shaowei
|
| 中文摘要 | 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
|
| 语种 | 英语
|
| 公开日期 | 2014-12-16
|
| 源URL | [http://ir.iscas.ac.cn/handle/311060/17024]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文
|
推荐引用方式
GB/T 7714 |
Cai, Shaowei ,Luo, Chuan ,Su, Kaile . 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 .(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.
|
