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.
Bibliographical noteFunding Information:
This work is supported by the National Natural Science Foundation of China (Grant No.61673320) and the Fundamental Research Funds for the Central Universities (Grant No.2682019ZT16 and No.2682020CX59), and Sichuan Science and Technology Program (Grant No. 2020YJ0270). The authors would like to thank Tomáš Balyo for providing the HRS generator.
This work is supported by the National Natural Science Foundation of China (Grant No.61673320) and the Fundamental Research Funds for the Central Universities (Grant No.2682017ZT12, 2682016 CX119).
© 2020, Springer Science+Business Media, LLC, part of Springer Nature.
Copyright 2020 Elsevier B.V., All rights reserved.
- Hard random satisfiability (HRS)
- Stochastic local search (SLS)
- Linear combination