More efficient stochastic local search for satisfiability

Huimin Fu, Guanfeng Wu, J. Liu, Yang Xu

Research output: Contribution to journalArticlepeer-review

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.
Original languageEnglish
Pages (from-to)1-20
Number of pages20
JournalApplied Intelligence
Volume0
Issue number0
Early online date25 Nov 2020
DOIs
Publication statusE-pub ahead of print - 25 Nov 2020

Bibliographical note

Funding 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.

Funding 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.2682017ZT12, 2682016 CX119).

Publisher Copyright:
© 2020, Springer Science+Business Media, LLC, part of Springer Nature.

Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.

Keywords

  • Hard random satisfiability (HRS)
  • Stochastic local search (SLS)
  • Linear combination
  • Property

Fingerprint

Dive into the research topics of 'More efficient stochastic local search for satisfiability'. Together they form a unique fingerprint.

Cite this