SAT solver
In spite of this, efficient and scalable algorithms for SAT were developed during the 2000s, which have contributed to dramatic advances in the ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints.
Most SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution, with an output such as "unknown" in the latter case.
Modern SAT solvers have had a significant impact on fields including software verification, program analysis, constraint solving, artificial intelligence, electronic design automation, and operations research.
SAT solvers are usually developed using one of two core approaches: the Davis–Putnam–Logemann–Loveland algorithm (DPLL) and conflict-driven clause learning (CDCL).
[2][3] Many modern approaches to practical SAT solving are derived from the DPLL algorithm and share the same structure.
[4] Conflict-driven solvers, such as conflict-driven clause learning (CDCL), augment the basic DPLL search algorithm with efficient conflict analysis, clause learning, backjumping, a "two-watched-literals" form of unit propagation, adaptive branching, and random restarts.
These "extras" to the basic systematic search have been empirically shown to be essential for handling the large SAT instances that arise in electronic design automation (EDA).
[citation needed] The conflict-driven MiniSAT, which was relatively successful at the 2005 SAT competition, only has about 600 lines of code.
Google's CP-SAT solver, part of OR-Tools, won gold medals at the Minizinc constraint programming competitions in 2018, 2019, 2020, and 2021.
Certain types of large random satisfiable instances of SAT can be solved by survey propagation (SP).
Each of them solves a copy of the SAT instance, whereas divide-and-conquer algorithms divide the problem between the processors.
In 2016,[11] 2017[12] and 2018,[13] the benchmarks were run on a shared-memory system with 24 processing cores, therefore solvers intended for distributed memory or manycore processors might have fallen short.
Other diversification strategies involve enabling, disabling or diversifying certain heuristics in the sequential solver.
[16][17] It was designed to find a lower bound for the performance a parallel SAT solver should be able to deliver.
Despite the large amount of duplicate work due to lack of optimizations, it performed well on a shared memory machine.
Particularly for hard SAT instances HordeSat can produce linear speedups and therefore reduce runtime significantly.
However, due to techniques like unit propagation, following a division, the partial problems may differ significantly in complexity.
Thus the DPLL algorithm typically does not process each part of the search space in the same amount of time, yielding a challenging load balancing problem.
The cutoff heuristic decides when to stop expanding a cube and instead forward it to a sequential conflict-driven solver.
[22] Cube-and-Conquer is a modification or a generalization of the DPLL-based Divide-and-conquer approach used to compute the Van der Waerden numbers w(2;3,17) and w(2;3,18) in 2010 [23] where both the phases (splitting and solving the partial problems) were performed using DPLL.
One strategy towards a parallel local search algorithm for SAT solving is trying multiple variable flips concurrently on different processing units.
Stochastic methods try to find a satisfying interpretation but cannot deduce that a SAT instance is unsatisfiable, as opposed to complete algorithms, such as DPLL.
In Ramsey theory, several previously unknown Van der Waerden numbers were computed with the help of specialized SAT solvers running on FPGAs.
[29][30] In 2016, Marijn Heule, Oliver Kullmann, and Victor Marek solved the Boolean Pythagorean triples problem by using a SAT solver to show that there is no way to color the integers up to 7825 in the required fashion.
[34][35] SAT solvers are the core component on which satisfiability modulo theories (SMT) solvers are built, which are used for problems such as job scheduling, symbolic execution, program model checking, program verification based on hoare logic, and other applications.
Other authors used this technology to prove new impossibilities about the no-show paradox, half-way monotonicity, and probabilistic voting rules.
Brandl, Brandt, Peters and Stricker used it to prove the impossibility of a strategyproof, efficient and fair rule for fractional social choice.
