Emphasis on the flipping variable: Towards effective local search for hard random satisfiability

Huimin Fu, Yang Xu, Guanfeng Wu, Jun Liu, Shuwei Chen, Xingxing He

Research output: Contribution to journalArticlepeer-review

9 Citations (Scopus)
94 Downloads (Pure)

Abstract

Uniform random satisfiability (URS) and hard random satisfiability (HRS) are two important benchmarks for algorithms that solve Boolean satisfiability problems, i.e., SAT solvers, especially for random SAT solvers. Recently, the stochastic local search (SLS) algorithms have made major breakthroughs in URS, resulting in several new 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 a new SLS algorithm, named EPEFV for HRS, which employs the extended framework of ProbSAT, and adds a new heuristic method that emphasizes the role of flipping variable, called EFV. EFV focuses on the flipping variables and is based on three components: 1) A new clause weighting scheme focusing on the flipping variable, which is based on a new clause property called UnsatT. By applying this new weighting scheme and a biased random walk, we design a new clause selection mechanism. 2) Design a new scoring function named Uv by combining a novel variable property vUnsatT based on the flipping variable with the commonly used property score.3) A new tie-breaking strategy in the variable selection mechanism based on the new scoring function Uv. Extensive experimental results demonstrate that EPEFV can not only greatly outperforms the state-of-the-art SLS algorithms as well as complete solver competitors on HRS instances, but also can effectively solve URS instances with long clauses. On the contrary, the most advanced SLS solvers, however, can only effectively solve URS instances, while the most advanced complete solvers can only effectively solve HRS instances. At present, no solver can effectively solve both HRS and URS at the same time, which means that the EPEFV can be regarded as the state-of-the-art SLS solver for both HRS instances and URS instances with long clauses. Finally, further empirical analysis confirms the effectiveness of each mechanism underlying the EFV heuristic on HRS instances.
Original languageEnglish
Pages (from-to)118-139
Number of pages22
JournalInformation Sciences
Volume566
Early online date17 Mar 2021
DOIs
Publication statusPublished (in print/issue) - 31 Aug 2021

Bibliographical note

Funding Information:
This work is supported by the National Natural Science Foundation of China (Grant No. 61673320 ), Sichuan Science and Technology Program (Grant No. 2020YJ0270 ), Humanities and Social Sciences Research Project of the Ministry of Education of China (Grant No. 20XJCZH016 ), and the Fundamental Research Funds for the Central Universities (Grant No. 2682019ZT16 , Grant No. 2682020CX59 ). The authors would like to thank Tomas Balyo for providing the HRS generator.

Publisher Copyright:
© 2021 Elsevier Inc.

Keywords

  • Satisfiability (SAT) problem
  • Selection mechanism
  • Stochastic local search (SLS)
  • Weighting scheme

Fingerprint

Dive into the research topics of 'Emphasis on the flipping variable: Towards effective local search for hard random satisfiability'. Together they form a unique fingerprint.

Cite this