Zchaff2004: An Efficient SAT Solver

2005 ◽  
pp. 360-375 ◽  
Author(s):  
Yogesh S. Mahajan ◽  
Zhaohui Fu ◽  
Sharad Malik
Keyword(s):  
Sat Solver

An Efficient Local Search SAT Solver with Effective Preprocessing for Structured Instances

2021 ◽  
Vol 2 (2) ◽  
Author(s):  
Md Shibbir Hossen ◽  
Md Masbaul Alam Polash
Keyword(s):  
Local Search ◽  
Sat Solver

scholarly journals A Flexible Proof Format for SAT Solver-Elaborator Communication

2021 ◽  
pp. 59-75
Author(s):  
Seulkee Baek ◽  
Mario Carneiro ◽  
Marijn J. H. Heule
Keyword(s):  
Computational Cost ◽  
Memory Usage ◽  
Median Reduction ◽  
Implementation Effort ◽  
Sat Solver ◽  
Proof Methods

AbstractWe introduce , a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to , the format allows solvers to include more information in proofs to reduce the computational cost of subsequent elaboration to . The format is easy to parse forward and backward, and it is extensible to future proof methods. The provision of optional proof steps allows SAT solver developers to balance implementation effort against elaboration time, with little to no overhead on solver time. We benchmark our toolchain against a comparable toolchain and confirm >84% median reduction in elaboration time and >94% median decrease in peak memory usage.

scholarly journals Dolius: A Distributed Parallel SAT Solving Framework

10.29007/hvqt ◽  
2018 ◽  
Author(s):  
Gilles Audemard ◽  
Benoît Hoessen ◽  
Saïd Jabbour ◽  
Cédric Piette
Keyword(s):  
Shared Memory ◽  
State Of The Art ◽  
Divide And Conquer ◽  
Sat Solving ◽  
Sat Solvers ◽  
Sat Solver

Over the years, parallel SAT solving becomes more and more important. However, most of state-of-the-art parallel SAT solvers are portfolio-based ones. They aim at running several times the same solver with different parameters. In this paper, we propose a tool called Dolius, mainly based on the divide and conquer paradigm. In contrast to most current parallel efficient engines, Dolius does not need shared memory, can be distributed, and scales well when a large number of computing units is available. Furthermore, our tool contains an API allowing to plug any SAT solver in a simple way.

Sign in / Sign up

Export Citation Format

Share Document