Abstract
Boolean Satisfiability problem (SAT) plays a prominent role in many domains of computer science and artificial
intelligence due to its significant importance in both theory and applications. Algorithms for solving SAT problems
can be categorized into two main classes: complete algorithms and incomplete algorithms (typically stochastic local
search (SLS) algorithms). SLS algorithms are among the most effective for solving uniform random SAT problems,
while hybrid algorithms achieved great breakthroughs for solving hard random SAT (HRS) problem recently.
However, there is a lack of algorithms that can effectively solve both uniform random SAT and HRS problems. In
this paper, a new SLS algorithm named SelectNTS is proposed aiming at solving both uniform random SAT and HRS
problem effectively. SelectNTS is essentially an improved probability selection based local search algorithm, the core
of which includes new clause and variable selection heuristics: a new clause weighting scheme and a biased random
walk strategy are utilized to select a clause, while a new probability selection strategy with the variation of
configuration checking strategy is used to select a variable. Extensive experimental results show that SelectNTS
outperforms the state-of-the-art random SAT algorithms and hybrid algorithms in solving both uniform random SAT
and HRS problems effectively.
intelligence due to its significant importance in both theory and applications. Algorithms for solving SAT problems
can be categorized into two main classes: complete algorithms and incomplete algorithms (typically stochastic local
search (SLS) algorithms). SLS algorithms are among the most effective for solving uniform random SAT problems,
while hybrid algorithms achieved great breakthroughs for solving hard random SAT (HRS) problem recently.
However, there is a lack of algorithms that can effectively solve both uniform random SAT and HRS problems. In
this paper, a new SLS algorithm named SelectNTS is proposed aiming at solving both uniform random SAT and HRS
problem effectively. SelectNTS is essentially an improved probability selection based local search algorithm, the core
of which includes new clause and variable selection heuristics: a new clause weighting scheme and a biased random
walk strategy are utilized to select a clause, while a new probability selection strategy with the variation of
configuration checking strategy is used to select a variable. Extensive experimental results show that SelectNTS
outperforms the state-of-the-art random SAT algorithms and hybrid algorithms in solving both uniform random SAT
and HRS problems effectively.
Original language | English |
---|---|
Article number | 108572 |
Pages (from-to) | 1-17 |
Number of pages | 17 |
Journal | Knowledge-Based Systems |
Volume | 245 |
Early online date | 17 Mar 2022 |
DOIs | |
Publication status | Published (in print/issue) - 7 Jun 2022 |
Bibliographical note
Funding Information:This work is partially supported by National Natural Science Foundation of China (Grant No: 62106206), and Sichuan Science and Technology Program, China (Grant No. 2020YJ0270 ), and the Fundamental Research Funds for the Central Universities, China (Grant No. 2682017ZT12 , 2682016CX119 , 2682019ZT16 , 2682020CX59 ).
Publisher Copyright:
© 2022 Elsevier B.V.
Keywords
- Boolean Satisfiability problem
- Stochastic local search
- Weights