中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
Scoring functions based on second level score for κ-SAT with long clauses
Author: Cai, Shaowei (1) ; Luo, Chuan (3) ; Su, Kaile (4)
Corresponding Author: Cai, Shaowei
Source: Journal of Artificial Intelligence Research
Issued Date: 2014
Volume: 51, Pages:413-441
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
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.
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.
Language: 英语
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/17024
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
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-01-01,51:413-441.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Cai, Shaowei (1)]'s Articles
[Luo, Chuan (3)]'s Articles
[Su, Kaile (4)]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Cai, Shaowei (1)]‘s Articles
[Luo, Chuan (3)]‘s Articles
[Su, Kaile (4)]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2021  中国科学院软件研究所 - Feedback
Powered by CSpace