Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings

2006 ◽  
Vol 35 (1-3) ◽  
pp. 143-179 ◽  
Author(s):  
Alan M. Frisch ◽  
Timothy J. Peugniez ◽  
Anthony J. Doggett ◽  
Peter W. Nightingale
SAT 2005 ◽  
2007 ◽  
pp. 143-179 ◽  
Author(s):  
Alan M. Frisch ◽  
Timothy J. Peugniez ◽  
Anthony J. Doggett ◽  
Peter W. Nightingale

Author(s):  
Wenjie Zhang ◽  
Zeyu Sun ◽  
Qihao Zhu ◽  
Ge Li ◽  
Shaowei Cai ◽  
...  

The Boolean satisfiability problem (SAT) is a famous NP-complete problem in computer science. An effective way for solving a satisfiable SAT problem is the stochastic local search (SLS). However, in this method, the initialization is assigned in a random manner, which impacts the effectiveness of SLS solvers. To address this problem, we propose NLocalSAT. NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network. We evaluated NLocalSAT on five SLS solvers (CCAnr, Sparrow, CPSparrow, YalSAT, and probSAT) with instances in the random track of SAT Competition 2018. The experimental results show that solvers with NLocalSAT achieve 27% ~ 62% improvement over the original SLS solvers.


2018 ◽  
Vol 89 ◽  
pp. 68-81 ◽  
Author(s):  
Túlio A.M. Toffolo ◽  
Jan Christiaens ◽  
Sam Van Malderen ◽  
Tony Wauters ◽  
Greet Vanden Berghe

2008 ◽  
Vol 105 (40) ◽  
pp. 15253-15257 ◽  
Author(s):  
Mikko Alava ◽  
John Ardelius ◽  
Erik Aurell ◽  
Petteri Kaski ◽  
Supriya Krishnamurthy ◽  
...  

We study the performance of stochastic local search algorithms for random instances of the K-satisfiability (K-SAT) problem. We present a stochastic local search algorithm, ChainSAT, which moves in the energy landscape of a problem instance by never going upwards in energy. ChainSAT is a focused algorithm in the sense that it focuses on variables occurring in unsatisfied clauses. We show by extensive numerical investigations that ChainSAT and other focused algorithms solve large K-SAT instances almost surely in linear time, up to high clause-to-variable ratios α; for example, for K = 4 we observe linear-time performance well beyond the recently postulated clustering and condensation transitions in the solution space. The performance of ChainSAT is a surprise given that by design the algorithm gets trapped into the first local energy minimum it encounters, yet no such minima are encountered. We also study the geometry of the solution space as accessed by stochastic local search algorithms.


2017 ◽  
Vol 44 (4) ◽  
pp. 32-37
Author(s):  
Shohei Sassa ◽  
Kenji Kanazawa ◽  
Shaowei Cai ◽  
Moritoshi Yasunaga

Sign in / Sign up

Export Citation Format

Share Document