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

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