More efficient stochastic local search for satisfiability
- PDF / 1,001,948 Bytes
- 20 Pages / 595.276 x 790.866 pts Page_size
- 2 Downloads / 246 Views
More efficient stochastic local search for satisfiability Huimin Fu 1 & Guanfeng Wu 2 & Jun Liu 3 & Yang Xu 2 Accepted: 25 September 2020 # Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Uniform random satisfiability (URS) and hard random satisfiability (HRS) are two significant generalizations of random satisfiability (RS). Recently, great breakthroughs have been made on stochastic local search (SLS) algorithms for uniform RS, resulting in several state-of-the-art algorithms, e.g., Dimetheus, YalSAT, ProbSAT and Score2SAT. However, compared to the great progress of SLS on URS, the performance of SLS on HRS lags far behind. In this paper, we propose two global clause weighting schemes and a new hybrid scoring function called SA based on a linear combination of a property score and property age, and then apply a second-level-biased random walk strategy based on two clause weighting schemes and SA to develop a new SLS solver called BRSAP. To evaluate the performance of BRSAP, we conduct extensive experiments to compare BRSAP with state-of-the-art SLS solvers and complete solvers on HRS instances and URS instances from SAT Competition 2017 and SAT Competition 2018 as well as 4100 generated satisfiable large HRS and URS ones. The experiments illustrate that BRSAP obviously outperforms its competitors, indicating the effectiveness of BRSAP. We also analyze the effectiveness of the underlying ideas in BRSAP. Keywords Hard random satisfiability (HRS) . Stochastic local search (SLS) . Linear combination . Property
1 Introduction The propositional satisfiability (SAT) problem is one of the most widely studied NP-complete problems, and plays an outstanding role in many domains of computer science and * Guanfeng Wu [email protected] Huimin Fu [email protected] Jun Liu [email protected] Yang Xu [email protected] 1
Key Laboratory of National-Local Joint Engineering Laboratory of System Credibility Automatic Verification of China, School of Information Science and Technology, Southwest Jiaotong University, Chengdu, China
2
Key Laboratory of National-Local Joint Engineering Laboratory of System Credibility Automatic Verification of China, School of Mathematic, Chengdu, China
3
Key Laboratory of National-Local Joint Engineering Laboratory of System Credibility Automatic Verification of China, and also with the School of Computing, Ulster University, Northern Ireland, UK
artificial intelligence, due to its significant importance in both theory and applications [1]. The SAT problem is fundamental in solving many practical problems in combinatorial optimization, statistical physics, circuit verification, computing theory [2, 3], and SAT algorithms have been widely used to solve real-world applications, such as computer algebra systems [4], core computer algebra systems [5], core graphs [6], gene regulatory networks [7], automated verification [8], model-based diagnosis (MBD) [9], scheduling [10], and machine induction [11]. There are many optimization algorithms dedicated to differen
Data Loading...
