| Scoring functions based on second level score for κ-SAT with long clauses |
| Cai, Shaowei (1); Luo, Chuan (3); Su, Kaile (4); Cai, Shaowei
|
| 2014
|
| Source | Journal of Artificial Intelligence Research
 |
| ISSN | 10769757
|
| Volume | 51Pages:413-441 |
| English Abstract | 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. |
| Indexed Type | EI
|
| Department | (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
|
| Language | 英语
|
| Content Type | 期刊论文
|
| URI | http://ir.iscas.ac.cn/handle/311060/17024
|
| Collection | 中国科学院软件研究所
|
| Corresponding Author | Cai, Shaowei |
Recommended Citation
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.
|
| Files in This Item: |
|
There are no files associated with this item. |
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment