2302:
486:
the ideal form for a conflict-driven solver. Furthermore, look-ahead solvers consider the entire problem whereas conflict-driven solvers make decisions based on information that is much more local. There are three heuristics involved in the cube phase. The variables in the cubes are chosen by the decision heuristic. The direction heuristic decides which variable assignment (true or false) to explore first. In satisfiable problem instances, choosing a satisfiable branch first is beneficial. The cutoff heuristic decides when to stop expanding a cube and instead forward it to a sequential conflict-driven solver. Preferably the cubes are similarly complex to solve.
405:
will solve this instance particularly fast. These limitations motivate the parallel portfolio approach. A portfolio is a set of different algorithms or different configurations of the same algorithm. All solvers in a parallel portfolio run on different processors to solve of the same problem. If one solver terminates, the portfolio solver reports the problem to be satisfiable or unsatisfiable according to this one solver. All other solvers are terminated. Diversifying portfolios by including a variety of solvers, each performing well on a different set of problems, increases the robustness of the solver.
420:
makes a competitive parallel solver. An example of such a solver is PPfolio. 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. HordeSat is a parallel portfolio solver for large clusters of computing nodes. It uses differently configured instances of the same sequential solver at its core. Particularly for hard SAT instances HordeSat can produce linear speedups and therefore reduce runtime significantly.
440:
2856:
2876:
2866:
288:. Many modern approaches to practical SAT solving are derived from the DPLL algorithm and share the same structure. Often they only improve the efficiency of certain classes of SAT problems such as instances that appear in industrial applications or randomly generated instances. Theoretically, exponential lower bounds have been proved for the DPLL family of algorithms.
133:, but incorporate a number of extensions and features. 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". Often, SAT solvers do not just provide an answer, but can provide further information including an example assignment (values for
431:
In contrast to parallel portfolios, parallel divide-and-conquer tries to split the search space between the processing elements. Divide-and-conquer algorithms, such as the sequential DPLL, already apply the technique of splitting the search space, hence their extension towards a parallel algorithm is
404:
In general there is no SAT solver that performs better than all other solvers on all SAT problems. An algorithm might perform well for problem instances others struggle with, but will do worse with other instances. Furthermore, given a SAT instance, there is no reliable way to predict which algorithm
333:
The conflict-driven MiniSAT, which was relatively successful at the 2005 SAT competition, only has about 600 lines of code. A modern
Parallel SAT solver is ManySAT. It can achieve super linear speed-ups on important classes of problems. An example for look-ahead solvers is march_dl, which won a prize
121:
problem in general. As a result, only algorithms with exponential worst-case complexity are known. 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
419:
One drawback of parallel portfolios is the amount of duplicate work. If clause learning is used in the sequential solvers, sharing learned clauses between parallel running solvers can reduce duplicate work and increase performance. Yet, even merely running a portfolio of the best solvers in parallel
485:
to the original formula, the problem is reported to be satisfiable, if one of the formulas is satisfiable. The look-ahead solver is favorable for small but hard problems, so it is used to gradually divide the problem into multiple sub-problems. These sub-problems are easier but still large which is
509:
One strategy towards a parallel local search algorithm for SAT solving is trying multiple variable flips concurrently on different processing units. Another is to apply the aforementioned portfolio approach, however clause sharing is not possible since local search solvers do not produce clauses.
283:
A DPLL SAT solver employs a systematic backtracking search procedure to explore the (exponentially sized) space of variable assignments looking for satisfying assignments. The basic search procedure was proposed in two seminal papers in the early 1960s (see references below) and is now commonly
329:
Look-ahead solvers have especially strengthened reductions (going beyond unit-clause propagation) and the heuristics, and they are generally stronger than conflict-driven solvers on hard instances (while conflict-driven solvers can be much better on large instances which actually have an easy
432:
straight forward. 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
376:
algorithms. With parallel portfolios, multiple different SAT solvers run concurrently. Each of them solves a copy of the SAT instance, whereas divide-and-conquer algorithms divide the problem between the processors. Different approaches exist to parallelize local search algorithms.
471:
paradigm. It suggests solving in two phases. In the "cube" phase the
Problem is divided into many thousands, up to millions, of sections. This is done by a look-ahead solver, that finds a set of partial configurations called "cubes". A cube can also be seen as a
489:
Treengeling is an example for a parallel solver that applies the Cube-and-Conquer paradigm. Since its introduction in 2012 it has had multiple successes at the
International SAT Solver Competition. Cube-and-Conquer was used to solve the
510:
Alternatively, it is possible to share the configurations that are produced locally. These configurations can be used to guide the production of a new initial configuration when a local solver decides to restart its search.
476:
of a subset of variables of the original formula. In conjunction with the formula, each of the cubes forms a new formula. These formulas can be solved independently and concurrently by conflict-driven solvers. As the
356:
Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. All of these behaviors can be seen in the SAT solving contests.
731:
and other classic impossibility theorems. Geist and
Endriss used it to find new impossibilities related to set extensions. Brandt and Geist used this approach to prove an impossibility about strategyproof
463:. The decision heuristic chooses which variables (circles) to assign. After the cutoff heuristic decides to stop further branching, the partial problems (rectangles) are solved independently using CDCL.
423:
In recent years parallel portfolio SAT solvers have dominated the parallel track of the
International SAT Solver Competitions. Notable examples of such solvers include Plingeling and painless-mcomsps.
612:
for 3-SAT. The latter is currently the fastest known algorithm for k-SAT at all values of k. In the setting with many satisfying assignments the randomized algorithm by Schöning has a better bound.
314:, 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
532:
In contrast, randomized algorithms like the PPSZ algorithm by Paturi, Pudlak, Saks, and Zane set variables in a random order according to some heuristics, for example bounded-width
2216:
2879:
2869:
610:
576:
for 3-SAT. This was the best-known runtime for this problem until 2019, when Hansen, Kaplan, Zamir and Zwick published a modification of that algorithm with a runtime of
574:
1737:
302:
Modern SAT solvers (developed in the 2000s) come in two flavors: "conflict-driven" and "look-ahead". Both approaches descend from DPLL. Conflict-driven solvers, such as
380:
The
International SAT Solver Competition has a parallel track reflecting recent advances in parallel SAT solving. In 2016, 2017 and 2018, the benchmarks were run on a
529:. 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.
2441:
416:
is a simple way to diversify a portfolio. Other diversification strategies involve enabling, disabling or diversifying certain heuristics in the sequential solver.
461:
349:
applications, satisfiability and other logical properties of a given propositional formula are sometimes decided based on a representation of the formula as a
2639:
2538:
262:
677:(in particular, bounded model checking), SAT solvers are used to check whether a finite-state system satisfies a specification of its intended behavior.
468:
1810:
Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016), "Solving and
Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer",
2521:
1094:
467:
Due to non-chronological backtracking, parallelization of conflict-driven clause learning is more difficult. One way to overcome this is the
2223:
1997:
1499:; Kullmann, Oliver; Marek, Victor W. (2016), "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer",
649:
by using a SAT solver to show that there is no way to color the integers up to 7825 in the required fashion. Small values of the
522:
501:
w(2;3,17) and w(2;3,18) in 2010 where both the phases (splitting and solving the partial problems) were performed using DPLL.
373:
2168:
1837:
1641:
1609:
1526:
1480:
1446:
1376:
1264:
1021:
949:
814:
964:
Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean
Satisfiability Solvers and Their Applications in Model Checking".
744:. Brandl, Brandt, Peters and Stricker used it to prove the impossibility of a strategyproof, efficient and fair rule for
646:
497:
Cube-and-Conquer is a modification or a generalization of the DPLL-based Divide-and-conquer approach used to compute the
491:
318:(EDA). Most state-of-the-art SAT solvers are based on the CDCL framework as of 2019. Well known implementations include
2905:
1429:; Kullmann, Oliver; Wieringa, Siert; Biere, Armin (2012), "Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads",
2478:
2024:
1688:
341:
Certain types of large random satisfiable instances of SAT can be solved by survey propagation (SP). Particularly in
141:, etc.) in case the formula is satisfiable or minimal set of unsatisfiable clauses if the formula is unsatisfiable.
2910:
728:
2577:
303:
297:
266:
153:
821:
modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables
249:
which asks, on input a
Boolean formula, to determine whether the formula is satisfiable or not. This problem is
2738:
2592:
2286:
2251:
1069:
767:
681:
536:. If the heuristic can't find the correct setting, the variable is assigned randomly. The PPSZ algorithm has a
185:
47:
2828:
2301:
169:
2791:
2310:
2261:
1349:
Balyo, Tomáš; Sanders, Peter; Sinz, Carsten (2015), "HordeSat: A Massively
Parallel Portfolio SAT Solver",
1280:
868:
369:
315:
173:
161:
2730:
1503:, Lecture Notes in Computer Science, vol. 9710, Springer International Publishing, pp. 228–245,
1353:, Lecture Notes in Computer Science, vol. 9340, Springer International Publishing, pp. 156–172,
2766:
2685:
741:
2796:
2516:
1196:
1172:
433:
17:
2088:
2859:
2387:
2209:
880:
727:, SAT solvers have been used to prove impossibility theorems. Tang and Lin used SAT solvers to prove
338:, won gold medals at the Minizinc constraint programming competitions in 2018, 2019, 2020, and 2021.
787:
Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Propagation = Lazy Clause Generation",
2710:
2508:
1596:, Lecture Notes in Computer Science, vol. 2470, Springer Berlin Heidelberg, pp. 714–719,
1325:
1117:
797:
745:
409:
306:(CDCL), augment the basic DPLL search algorithm with efficient conflict analysis, clause learning,
579:
543:
2900:
2670:
2426:
2418:
1628:, Lecture Notes in Computer Science, vol. 6683, Springer Berlin Heidelberg, pp. 46–60,
1433:, Lecture Notes in Computer Science, vol. 7261, Springer Berlin Heidelberg, pp. 50–65,
934:, Lecture Notes in Computer Science, vol. 2404, Springer Berlin Heidelberg, pp. 17–36,
762:
626:
385:
350:
157:
126:
1465:
2813:
2808:
2611:
2330:
930:
Zhang, Lintao; Malik, Sharad (2002), "The Quest for Efficient Boolean Satisfiability Solvers",
792:
701:
634:
498:
114:
2436:
2342:
2335:
1046:
670:
666:
346:
172:
and are built into some programming languages such as exposing SAT solvers as constraints in
145:
1996:
Biere, Armin; Cimatti, Alessandro; Clarke, Edmund M.; Strichman, Ofer; Zhu, Yunshan (2003).
2606:
2601:
2488:
2364:
2352:
2281:
1873:
1796:
1570:
1220:
757:
724:
107:
2126:
Peters, Dominik (2021). "Proportionality and Strategyproofness in Multiwinner Elections".
8:
2618:
2453:
2325:
733:
717:
662:
482:
478:
473:
393:
226:
consists of choosing, for each variable, an assignment TRUE or FALSE. For any assignment
165:
1877:
1624:
Arbelaez, Alejandro; Hamadi, Youssef (2011), "Improving Parallel Local Search for SAT",
82:
which make the formula true, or unsatisfiable, meaning that there are no such values of
2587:
2528:
2498:
2483:
2448:
2347:
2291:
2246:
2174:
2127:
2069:
1978:
1907:
1843:
1815:
1765:
1694:
1647:
1574:
1532:
1504:
1382:
1354:
1075:
1027:
981:
907:
850:
689:
650:
533:
446:
389:
365:
323:
230:, the Boolean formula can be evaluated, and evaluates to true or false. The formula is
2016:
1140:
2702:
2276:
2178:
2164:
2108:
2061:
2020:
1970:
1899:
1891:
1833:
1757:
1698:
1684:
1637:
1605:
1578:
1522:
1476:
1442:
1372:
1260:
1065:
1031:
1017:
945:
810:
705:
51:
2155:. EC '21. New York, NY, USA: Association for Computing Machinery. pp. 158–179.
2073:
1861:
1651:
1386:
985:
911:
854:
2649:
2548:
2473:
2382:
2232:
2156:
2147:
Brandl, Florian; Brandt, Felix; Peters, Dominik; Stricker, Christian (2021-07-18).
2100:
2053:
2012:
1982:
1962:
1911:
1881:
1847:
1825:
1769:
1753:
1749:
1676:
1629:
1597:
1558:
1536:
1514:
1434:
1364:
1301:
1252:
1109:
1079:
1057:
1009:
973:
935:
902:
897:
889:
842:
802:
311:
246:
149:
43:
31:
1665:
2753:
2543:
2463:
2372:
1829:
1792:
1566:
1549:
Ahmed, Tanbir (2010). "Two new van der Waerden numbers w(2;3,17) and w(2;3,18)".
1518:
1368:
1013:
1000:
833:
Davis, M.; Putnam, H. (1960). "A Computing Procedure for Quantification Theory".
806:
737:
342:
319:
250:
118:
2089:"Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers"
1633:
1592:
Roli, Andrea (2002), "Criticality and Parallelism in Structured SAT Instances",
1438:
1256:
2771:
2654:
2582:
2562:
2468:
2431:
2397:
2266:
2104:
977:
872:
720:, SAT solvers have been applied to solve optimization and scheduling problems.
693:
674:
285:
278:
130:
71:
35:
2149:"Distribution Rules Under Dichotomous Preferences: Two Out of Three Ain't Bad"
1966:
1886:
1680:
625:
SAT solvers have been used to assist in proving mathematical theorems through
194:
is any expression that can be written using Boolean (propositional) variables
94:
is true, so the solver should return "satisfiable". Since the introduction of
2894:
2458:
2392:
2256:
2112:
2065:
1974:
1895:
1761:
1601:
685:
630:
381:
2160:
2057:
1723:
1711:
1673:
40th Annual Symposium on Foundations of Computer Science (Cat. No.99CB37039)
940:
736:. Other authors used this technology to prove new impossibilities about the
2818:
2801:
2644:
2271:
1925:
1903:
1562:
1496:
1461:
1426:
642:
439:
2148:
2041:
1950:
1783:
Kouril, Michal (2012). "Computing the van der Waerden number W(3,4)=293".
1666:"A probabilistic algorithm for k-SAT and constraint satisfaction problems"
1061:
893:
846:
2634:
2493:
1949:
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan (2001-07-01).
1045:
Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S. (2001).
697:
413:
307:
1008:. Lecture Notes in Computer Science. Vol. 11628. pp. 250–266.
261:
SAT solvers are usually developed using one of two core approaches: the
2720:
1814:, Lecture Notes in Computer Science, vol. 9710, pp. 228–245,
1399:
791:, Lecture Notes in Computer Science, vol. 4741, pp. 544–558,
700:, and other applications. These techniques are also closely related to
519:
1113:
2781:
2597:
2377:
144:
Modern SAT solvers have had a significant impact on fields including
103:
95:
2680:
2201:
2153:
Proceedings of the 22nd ACM Conference on Economics and Computation
2132:
1820:
1509:
1359:
335:
99:
637:
were computed with the help of specialized SAT solvers running on
2675:
2533:
1152:
526:
98:
for SAT in the 1960s, modern SAT solvers have grown into complex
2195:
2042:"Satisfiability modulo theories: introduction and applications"
1247:
Balyo, Tomáš; Sinz, Carsten (2018), "Parallel Satisfiability",
1281:"Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010"
2833:
2823:
2743:
1351:
Theory and Applications of Satisfiability Testing -- SAT 2015
1054:
Proceedings of the 38th conference on Design automation (DAC)
999:
Möhle, Sibylle; Biere, Armin (2019). "Backing Backtracking".
684:(SMT) solvers are built, which are used for problems such as
334:
at the 2007 SAT competition. Google's CP-SAT solver, part of
1812:
Theory and Applications of Satisfiability Testing – SAT 2016
1501:
Theory and Applications of Satisfiability Testing – SAT 2016
1095:"GRASP: a search algorithm for propositional satisfiability"
1002:
Theory and Applications of Satisfiability Testing – SAT 2019
780:
122:
tens of thousands of variables and millions of constraints.
2786:
2761:
1995:
1594:
Principles and Practice of Constraint Programming - CP 2002
789:
Principles and Practice of Constraint Programming – CP 2007
638:
2146:
1425:
1326:"SAT 2011 Competition: 32 cores track: ranking of solvers"
198:
and the Boolean operations AND, OR, and NOT. For example,
1044:
518:
Algorithms that are not part of the DPLL family include
2776:
963:
27:
Computer program for the Boolean satisfiability problem
786:
129:. They are often based on core algorithms such as the
1951:"Bounded Model Checking Using Satisfiability Solving"
1717:
1092:
867:
582:
546:
449:
1251:, Springer International Publishing, pp. 3–29,
2040:De Moura, Leonardo; Bjørner, Nikolaj (2011-09-01).
1948:
1141:
http://www.cril.univ-artois.fr/~jabbour/manysat.htm
125:SAT solvers often begin by converting a formula to
1862:"Two-hundred-terabyte maths proof is largest ever"
1809:
1712:"An improved exponential-time algorithm for k-SAT"
1495:
604:
568:
455:
368:SAT solvers come in three categories: portfolio,
2892:
1348:
90:. In this case, the formula is satisfiable when
70:)", a SAT solver outputs whether the formula is
2086:
2039:
1738:"The van der Waerden Number $ W(2,6)$ Is 1132"
1460:
1431:Hardware and Software: Verification and Testing
653:were also computed by Heule using SAT solvers.
645:, Oliver Kullmann, and Victor Marek solved the
1705:
1623:
1093:Marques-Silva, J. P.; Sakallah, K. A. (1999).
2217:
2087:Coelho, José; Vanhoucke, Mario (2011-08-16).
1657:
1153:"The international SAT Competitions web page"
1047:"Chaff: Engineering an Efficient SAT Solver"
680:SAT solvers are the core component on which
168:. Powerful solvers are readily available as
74:, meaning that there are possible values of
1724:"Faster k-SAT algorithms using biased-PPSZ"
832:
656:
238:) for which the formula evaluates to true.
2875:
2865:
2224:
2210:
1776:
1735:
998:
929:
2131:
1885:
1819:
1508:
1358:
1249:Handbook of Parallel Constraint Reasoning
1246:
939:
901:
796:
2093:European Journal of Operational Research
1736:Kouril, Michal; Paul, Jerome L. (2008).
1663:
513:
438:
263:Davis–Putnam–Logemann–Loveland algorithm
234:if there exists an assignment (called a
873:"A machine program for theorem-proving"
14:
2893:
2125:
1782:
360:
2205:
1626:Learning and Intelligent Optimization
1548:
1421:
1419:
1242:
1240:
871:; Logemann, G.; Loveland, D. (1962).
426:
2231:
1859:
1591:
925:
923:
921:
647:Boolean Pythagorean triples problem
492:Boolean Pythagorean triples problem
310:, a "two-watched-literals" form of
24:
1489:
1416:
1237:
256:
25:
2922:
2189:
1278:
918:
711:
620:
388:, therefore solvers intended for
2874:
2864:
2855:
2854:
2300:
696:, program verification based on
2140:
2119:
2080:
2033:
1989:
1955:Formal Methods in System Design
1942:
1918:
1853:
1803:
1729:
1617:
1585:
1542:
1475:. IOS Press. pp. 155–184.
1454:
1392:
1342:
1318:
1294:
1272:
1213:
1189:
1165:
1145:
615:
504:
304:conflict-driven clause learning
298:Conflict-driven clause learning
267:conflict-driven clause learning
117:, Boolean satisfiability is an
2198:of Sat competitions since 2002
1754:10.1080/10586458.2008.10129025
1726:, Hansen, Kaplan, Zamir, Zwick
1466:"Look-Ahead Based SAT Solvers"
1134:
1102:IEEE Transactions on Computers
1086:
1038:
992:
957:
861:
826:
768:Satisfiability modulo theories
682:satisfiability modulo theories
599:
586:
563:
550:
408:Many solvers internally use a
243:Boolean satisfiability problem
186:Boolean satisfiability problem
48:Boolean satisfiability problem
13:
1:
2017:10.1016/S0065-2458(03)58003-2
773:
740:, half-way monotonicity, and
633:, several previously unknown
399:
170:free and open-source software
1830:10.1007/978-3-319-40970-2_15
1714:, Paturi, Pudlak, Saks, Zani
1519:10.1007/978-3-319-40970-2_15
1404:sat2018.forsyte.tuwien.ac.at
1369:10.1007/978-3-319-24318-4_12
1225:sat2018.forsyte.tuwien.ac.at
1014:10.1007/978-3-030-24258-9_18
807:10.1007/978-3-540-74970-7_39
605:{\displaystyle O(1.307^{n})}
569:{\displaystyle O(1.308^{n})}
316:electronic design automation
174:constraint logic programming
162:electronic design automation
102:involving a large number of
7:
2578:Curry–Howard correspondence
2029:– via Academic Press.
1860:Lamb, Evelyn (2016-06-01).
1634:10.1007/978-3-642-25566-3_4
1464:; van Maaren, Hans (2009).
1439:10.1007/978-3-642-34188-5_8
1257:10.1007/978-3-319-63516-3_1
932:Computer Aided Verification
751:
525:algorithms. One example is
443:Cube phase for the formula
179:
10:
2927:
2105:10.1016/j.ejor.2011.03.019
1664:Schöning, Uwe (Oct 1999).
1473:Handbook of Satisfiability
978:10.1109/JPROC.2015.2455034
742:probabilistic voting rules
295:
276:
183:
50:. On input a formula over
2906:Logic in computer science
2850:
2752:
2729:
2701:
2694:
2663:
2627:
2570:
2561:
2507:
2417:
2410:
2363:
2318:
2309:
2298:
2239:
2046:Communications of the ACM
1887:10.1038/nature.2016.19990
1681:10.1109/SFFCS.1999.814612
881:Communications of the ACM
396:might have fallen short.
113:By a result known as the
1998:"Bounded Model Checking"
1742:Experimental Mathematics
1602:10.1007/3-540-46135-3_51
746:fractional social choice
661:SAT solvers are used in
657:In software verification
46:which aims to solve the
2911:Satisfiability problems
2427:Abstract interpretation
2161:10.1145/3465456.3467653
2058:10.1145/1995376.1995394
1967:10.1023/A:1011276507260
1330:www.cril.univ-artois.fr
1306:www.cril.univ-artois.fr
966:Proceedings of the IEEE
941:10.1007/3-540-45657-0_2
903:2027/mdp.39015095248095
763:Computer-assisted proof
635:Van der Waerden numbers
627:computer-assisted proof
499:Van der Waerden numbers
410:random number generator
351:binary decision diagram
291:
272:
158:artificial intelligence
127:conjunctive normal form
1563:10.1515/integ.2010.032
1400:"SAT Competition 2018"
1221:"SAT Competition 2018"
1197:"SAT Competition 2017"
1173:"SAT Competition 2016"
702:constraint programming
606:
570:
464:
457:
2336:Categorical semantics
2005:Advances in Computers
1062:10.1145/378239.379017
894:10.1145/368273.368557
847:10.1145/321033.321034
607:
571:
514:Randomized approaches
481:of these formulas is
458:
442:
412:. Diversifying their
236:satisfying assignment
146:software verification
110:to work efficiently.
108:program optimizations
54:variables, such as "(
2282:Runtime verification
1675:. pp. 410–414.
758:Category:SAT solvers
734:tournament solutions
725:social choice theory
580:
544:
447:
2539:Invariant inference
2287:Safety and liveness
1926:"Schur Number Five"
1878:2016Natur.534...17L
1497:Heule, Marijn J. H.
1462:Heule, Marijn J. H.
1427:Heule, Marijn J. H.
718:operations research
663:formal verification
394:manycore processors
361:Parallel approaches
284:referred to as the
166:operations research
2703:Constraint solvers
2529:Concolic execution
2484:Symbolic execution
2292:Undefined behavior
2247:Control-flow graph
1201:baldur.iti.kit.edu
1177:baldur.iti.kit.edu
835:Journal of the ACM
690:symbolic execution
602:
566:
465:
453:
427:Divide-and-conquer
390:distributed memory
370:divide-and-conquer
330:instance inside).
154:constraint solving
115:Cook–Levin theorem
100:software artifacts
2888:
2887:
2846:
2845:
2842:
2841:
2557:
2556:
2406:
2405:
2170:978-1-4503-8554-1
2011:(2003): 117–148.
1930:www.cs.utexas.edu
1839:978-3-319-40969-6
1643:978-3-642-25565-6
1611:978-3-540-44120-5
1528:978-3-319-40969-6
1482:978-1-58603-929-5
1448:978-3-642-34187-8
1378:978-3-319-24317-7
1266:978-3-319-63515-6
1114:10.1109/12.769433
1023:978-3-030-24257-2
972:(11): 2021–2035.
951:978-3-540-43997-4
816:978-3-540-74969-1
706:logic programming
456:{\displaystyle F}
16:(Redirected from
2918:
2878:
2877:
2868:
2867:
2858:
2857:
2754:Proof assistants
2699:
2698:
2568:
2567:
2415:
2414:
2388:Rewriting system
2383:Process calculus
2316:
2315:
2304:
2233:Program analysis
2226:
2219:
2212:
2203:
2202:
2183:
2182:
2144:
2138:
2137:
2135:
2123:
2117:
2116:
2084:
2078:
2077:
2037:
2031:
2030:
2002:
1993:
1987:
1986:
1946:
1940:
1939:
1937:
1936:
1922:
1916:
1915:
1889:
1857:
1851:
1850:
1823:
1807:
1801:
1800:
1780:
1774:
1773:
1733:
1727:
1721:
1715:
1709:
1703:
1702:
1670:
1661:
1655:
1654:
1621:
1615:
1614:
1589:
1583:
1582:
1546:
1540:
1539:
1512:
1493:
1487:
1486:
1470:
1458:
1452:
1451:
1423:
1414:
1413:
1411:
1410:
1396:
1390:
1389:
1362:
1346:
1340:
1339:
1337:
1336:
1322:
1316:
1315:
1313:
1312:
1302:"ppfolio solver"
1298:
1292:
1291:
1285:
1276:
1270:
1269:
1244:
1235:
1234:
1232:
1231:
1217:
1211:
1210:
1208:
1207:
1193:
1187:
1186:
1184:
1183:
1169:
1163:
1162:
1160:
1159:
1149:
1143:
1138:
1132:
1131:
1129:
1128:
1122:
1116:. Archived from
1099:
1090:
1084:
1083:
1051:
1042:
1036:
1035:
1007:
996:
990:
989:
961:
955:
954:
943:
927:
916:
915:
905:
877:
865:
859:
858:
830:
824:
823:
800:
784:
611:
609:
608:
603:
598:
597:
575:
573:
572:
567:
562:
561:
539:
469:Cube-and-Conquer
462:
460:
459:
454:
386:processing cores
312:unit propagation
247:decision problem
150:program analysis
44:computer program
32:computer science
21:
2926:
2925:
2921:
2920:
2919:
2917:
2916:
2915:
2891:
2890:
2889:
2884:
2838:
2748:
2725:
2690:
2664:Data structures
2659:
2623:
2553:
2544:Program slicing
2503:
2402:
2373:Lambda calculus
2359:
2305:
2296:
2257:Hyperproperties
2235:
2230:
2192:
2187:
2186:
2171:
2145:
2141:
2124:
2120:
2085:
2081:
2038:
2034:
2027:
2000:
1994:
1990:
1947:
1943:
1934:
1932:
1924:
1923:
1919:
1872:(7605): 17–18.
1858:
1854:
1840:
1808:
1804:
1781:
1777:
1734:
1730:
1722:
1718:
1710:
1706:
1691:
1668:
1662:
1658:
1644:
1622:
1618:
1612:
1590:
1586:
1547:
1543:
1529:
1494:
1490:
1483:
1468:
1459:
1455:
1449:
1424:
1417:
1408:
1406:
1398:
1397:
1393:
1379:
1347:
1343:
1334:
1332:
1324:
1323:
1319:
1310:
1308:
1300:
1299:
1295:
1283:
1277:
1273:
1267:
1245:
1238:
1229:
1227:
1219:
1218:
1214:
1205:
1203:
1195:
1194:
1190:
1181:
1179:
1171:
1170:
1166:
1157:
1155:
1151:
1150:
1146:
1139:
1135:
1126:
1124:
1120:
1097:
1091:
1087:
1072:
1056:. p. 530.
1049:
1043:
1039:
1024:
1005:
997:
993:
962:
958:
952:
928:
919:
875:
866:
862:
831:
827:
817:
785:
781:
776:
754:
738:no-show paradox
729:Arrow's theorem
714:
659:
623:
618:
593:
589:
581:
578:
577:
557:
553:
545:
542:
541:
537:
516:
507:
448:
445:
444:
429:
402:
384:system with 24
363:
343:hardware design
300:
294:
281:
275:
259:
257:Core algorithms
192:Boolean formula
188:
182:
28:
23:
22:
15:
12:
11:
5:
2924:
2914:
2913:
2908:
2903:
2901:Formal methods
2886:
2885:
2883:
2882:
2872:
2862:
2851:
2848:
2847:
2844:
2843:
2840:
2839:
2837:
2836:
2831:
2826:
2821:
2816:
2811:
2806:
2805:
2804:
2794:
2789:
2784:
2779:
2774:
2769:
2764:
2758:
2756:
2750:
2749:
2747:
2746:
2741:
2735:
2733:
2727:
2726:
2724:
2723:
2718:
2713:
2707:
2705:
2696:
2692:
2691:
2689:
2688:
2683:
2678:
2673:
2667:
2665:
2661:
2660:
2658:
2657:
2652:
2647:
2642:
2637:
2631:
2629:
2625:
2624:
2622:
2621:
2616:
2615:
2614:
2604:
2595:
2590:
2585:
2583:Loop invariant
2580:
2574:
2572:
2565:
2563:Formal methods
2559:
2558:
2555:
2554:
2552:
2551:
2546:
2541:
2536:
2531:
2526:
2525:
2524:
2522:Taint tracking
2513:
2511:
2505:
2504:
2502:
2501:
2496:
2491:
2486:
2481:
2476:
2471:
2469:Model checking
2466:
2461:
2456:
2451:
2446:
2445:
2444:
2434:
2429:
2423:
2421:
2412:
2408:
2407:
2404:
2403:
2401:
2400:
2398:Turing machine
2395:
2390:
2385:
2380:
2375:
2369:
2367:
2361:
2360:
2358:
2357:
2356:
2355:
2350:
2340:
2339:
2338:
2328:
2322:
2320:
2313:
2307:
2306:
2299:
2297:
2295:
2294:
2289:
2284:
2279:
2277:Rice's theorem
2274:
2269:
2267:Path explosion
2264:
2259:
2254:
2249:
2243:
2241:
2237:
2236:
2229:
2228:
2221:
2214:
2206:
2200:
2199:
2191:
2190:External links
2188:
2185:
2184:
2169:
2139:
2118:
2079:
2032:
2025:
1988:
1941:
1917:
1852:
1838:
1802:
1775:
1728:
1716:
1704:
1689:
1656:
1642:
1616:
1610:
1584:
1557:(4): 369–377.
1541:
1527:
1488:
1481:
1453:
1447:
1415:
1391:
1377:
1341:
1317:
1293:
1279:Biere, Armin.
1271:
1265:
1236:
1212:
1188:
1164:
1144:
1133:
1085:
1070:
1037:
1022:
991:
956:
950:
917:
888:(7): 394–397.
860:
825:
815:
798:10.1.1.70.5471
778:
777:
775:
772:
771:
770:
765:
760:
753:
750:
713:
712:In other areas
710:
694:model checking
686:job scheduling
675:model checking
658:
655:
622:
621:In mathematics
619:
617:
614:
601:
596:
592:
588:
585:
565:
560:
556:
552:
549:
515:
512:
506:
503:
452:
434:load balancing
428:
425:
401:
398:
362:
359:
296:Main article:
293:
290:
286:DPLL algorithm
279:DPLL algorithm
277:Main article:
274:
271:
258:
255:
220:
219:
184:Main article:
181:
178:
131:DPLL algorithm
36:formal methods
26:
9:
6:
4:
3:
2:
2923:
2912:
2909:
2907:
2904:
2902:
2899:
2898:
2896:
2881:
2873:
2871:
2863:
2861:
2853:
2852:
2849:
2835:
2832:
2830:
2827:
2825:
2822:
2820:
2817:
2815:
2812:
2810:
2807:
2803:
2800:
2799:
2798:
2795:
2793:
2790:
2788:
2785:
2783:
2780:
2778:
2775:
2773:
2770:
2768:
2765:
2763:
2760:
2759:
2757:
2755:
2751:
2745:
2742:
2740:
2737:
2736:
2734:
2732:
2728:
2722:
2719:
2717:
2714:
2712:
2709:
2708:
2706:
2704:
2700:
2697:
2693:
2687:
2684:
2682:
2679:
2677:
2674:
2672:
2669:
2668:
2666:
2662:
2656:
2653:
2651:
2648:
2646:
2643:
2641:
2640:Incorrectness
2638:
2636:
2633:
2632:
2630:
2626:
2620:
2617:
2613:
2610:
2609:
2608:
2607:Specification
2605:
2603:
2599:
2596:
2594:
2591:
2589:
2586:
2584:
2581:
2579:
2576:
2575:
2573:
2569:
2566:
2564:
2560:
2550:
2547:
2545:
2542:
2540:
2537:
2535:
2532:
2530:
2527:
2523:
2520:
2519:
2518:
2515:
2514:
2512:
2510:
2506:
2500:
2497:
2495:
2492:
2490:
2487:
2485:
2482:
2480:
2477:
2475:
2472:
2470:
2467:
2465:
2462:
2460:
2459:Effect system
2457:
2455:
2452:
2450:
2447:
2443:
2440:
2439:
2438:
2435:
2433:
2430:
2428:
2425:
2424:
2422:
2420:
2416:
2413:
2409:
2399:
2396:
2394:
2393:State machine
2391:
2389:
2386:
2384:
2381:
2379:
2376:
2374:
2371:
2370:
2368:
2366:
2362:
2354:
2351:
2349:
2346:
2345:
2344:
2341:
2337:
2334:
2333:
2332:
2329:
2327:
2324:
2323:
2321:
2317:
2314:
2312:
2308:
2303:
2293:
2290:
2288:
2285:
2283:
2280:
2278:
2275:
2273:
2270:
2268:
2265:
2263:
2260:
2258:
2255:
2253:
2250:
2248:
2245:
2244:
2242:
2238:
2234:
2227:
2222:
2220:
2215:
2213:
2208:
2207:
2204:
2197:
2194:
2193:
2180:
2176:
2172:
2166:
2162:
2158:
2154:
2150:
2143:
2134:
2129:
2122:
2114:
2110:
2106:
2102:
2098:
2094:
2090:
2083:
2075:
2071:
2067:
2063:
2059:
2055:
2051:
2047:
2043:
2036:
2028:
2026:9780120121588
2022:
2018:
2014:
2010:
2006:
1999:
1992:
1984:
1980:
1976:
1972:
1968:
1964:
1960:
1956:
1952:
1945:
1931:
1927:
1921:
1913:
1909:
1905:
1901:
1897:
1893:
1888:
1883:
1879:
1875:
1871:
1867:
1863:
1856:
1849:
1845:
1841:
1835:
1831:
1827:
1822:
1817:
1813:
1806:
1798:
1794:
1790:
1786:
1779:
1771:
1767:
1763:
1759:
1755:
1751:
1747:
1743:
1739:
1732:
1725:
1720:
1713:
1708:
1700:
1696:
1692:
1690:0-7695-0409-4
1686:
1682:
1678:
1674:
1667:
1660:
1653:
1649:
1645:
1639:
1635:
1631:
1627:
1620:
1613:
1607:
1603:
1599:
1595:
1588:
1580:
1576:
1572:
1568:
1564:
1560:
1556:
1552:
1545:
1538:
1534:
1530:
1524:
1520:
1516:
1511:
1506:
1502:
1498:
1492:
1484:
1478:
1474:
1467:
1463:
1457:
1450:
1444:
1440:
1436:
1432:
1428:
1422:
1420:
1405:
1401:
1395:
1388:
1384:
1380:
1374:
1370:
1366:
1361:
1356:
1352:
1345:
1331:
1327:
1321:
1307:
1303:
1297:
1289:
1288:SAT-RACE 2010
1282:
1275:
1268:
1262:
1258:
1254:
1250:
1243:
1241:
1226:
1222:
1216:
1202:
1198:
1192:
1178:
1174:
1168:
1154:
1148:
1142:
1137:
1123:on 2016-11-04
1119:
1115:
1111:
1107:
1103:
1096:
1089:
1081:
1077:
1073:
1067:
1063:
1059:
1055:
1048:
1041:
1033:
1029:
1025:
1019:
1015:
1011:
1004:
1003:
995:
987:
983:
979:
975:
971:
967:
960:
953:
947:
942:
937:
933:
926:
924:
922:
913:
909:
904:
899:
895:
891:
887:
883:
882:
874:
870:
864:
856:
852:
848:
844:
840:
836:
829:
822:
818:
812:
808:
804:
799:
794:
790:
783:
779:
769:
766:
764:
761:
759:
756:
755:
749:
747:
743:
739:
735:
730:
726:
721:
719:
709:
707:
703:
699:
695:
691:
687:
683:
678:
676:
672:
668:
664:
654:
652:
651:Schur numbers
648:
644:
640:
636:
632:
631:Ramsey theory
628:
613:
594:
590:
583:
558:
554:
547:
535:
530:
528:
524:
521:
511:
502:
500:
495:
493:
487:
484:
480:
475:
470:
450:
441:
437:
435:
424:
421:
417:
415:
411:
406:
397:
395:
391:
387:
383:
382:shared-memory
378:
375:
372:and parallel
371:
367:
358:
354:
352:
348:
344:
339:
337:
331:
327:
325:
321:
317:
313:
309:
305:
299:
289:
287:
280:
270:
268:
264:
254:
252:
248:
244:
239:
237:
233:
229:
225:
217:
213:
209:
205:
201:
200:
199:
197:
193:
187:
177:
175:
171:
167:
163:
159:
155:
151:
147:
142:
140:
136:
132:
128:
123:
120:
116:
111:
109:
105:
101:
97:
93:
89:
85:
81:
77:
73:
69:
65:
61:
57:
53:
49:
45:
41:
37:
33:
19:
2802:Isabelle/HOL
2715:
2619:Verification
2602:completeness
2494:Type systems
2437:Control flow
2331:Denotational
2272:Polyvariance
2240:Key concepts
2152:
2142:
2121:
2099:(1): 73–82.
2096:
2092:
2082:
2052:(9): 69–77.
2049:
2045:
2035:
2008:
2004:
1991:
1958:
1954:
1944:
1933:. Retrieved
1929:
1920:
1869:
1865:
1855:
1811:
1805:
1788:
1784:
1778:
1748:(1): 53–61.
1745:
1741:
1731:
1719:
1707:
1672:
1659:
1625:
1619:
1593:
1587:
1554:
1550:
1544:
1500:
1491:
1472:
1456:
1430:
1407:. Retrieved
1403:
1394:
1350:
1344:
1333:. Retrieved
1329:
1320:
1309:. Retrieved
1305:
1296:
1287:
1274:
1248:
1228:. Retrieved
1224:
1215:
1204:. Retrieved
1200:
1191:
1180:. Retrieved
1176:
1167:
1156:. Retrieved
1147:
1136:
1125:. Retrieved
1118:the original
1105:
1101:
1088:
1053:
1040:
1001:
994:
969:
965:
959:
931:
885:
879:
863:
838:
834:
828:
820:
788:
782:
722:
715:
679:
660:
643:Marijn Heule
624:
616:Applications
531:
523:local search
517:
508:
505:Local search
496:
488:
466:
430:
422:
418:
407:
403:
379:
374:local search
364:
355:
347:verification
340:
332:
328:
301:
282:
260:
242:
240:
235:
231:
227:
223:
221:
215:
211:
207:
203:
196:x, y, z, ...
195:
191:
189:
143:
138:
134:
124:
112:
91:
87:
83:
79:
75:
67:
63:
59:
55:
39:
29:
2731:Lightweight
2593:Side effect
2489:Termination
2343:Operational
2252:Correctness
1961:(1): 7–34.
698:hoare logic
641:. In 2016,
479:disjunction
474:conjunction
308:backjumping
265:(DPLL) and
251:NP-complete
232:satisfiable
119:NP-complete
72:satisfiable
2895:Categories
2686:Union-find
2650:Separation
2588:Refinement
2454:Dependence
2353:Small-step
2262:Invariants
2133:2104.08594
1935:2023-10-26
1821:1605.00723
1510:1605.00723
1409:2020-02-13
1360:1505.03340
1335:2020-02-13
1311:2019-12-29
1230:2020-02-13
1206:2020-02-13
1182:2020-02-13
1158:2007-11-15
1127:2015-08-28
1108:(5): 506.
1071:1581132972
841:(3): 201.
774:References
692:, program
534:resolution
520:stochastic
483:equivalent
400:Portfolios
224:assignment
104:heuristics
96:algorithms
40:SAT solver
18:SAT Solver
2782:HOL Light
2612:Languages
2598:Soundness
2517:Data-flow
2499:Typestate
2449:Data-flow
2378:Petri net
2326:Axiomatic
2311:Semantics
2179:232109303
2113:0377-2217
2066:0001-0782
1975:1572-8102
1896:1476-4687
1762:1058-6458
1699:123177576
1579:124272560
1032:195755607
869:Davis, M.
793:CiteSeerX
436:problem.
214:AND (NOT
2880:Glossary
2860:Category
2797:Isabelle
2681:Hashcons
2655:Temporal
2571:Concepts
2411:Analyses
2348:Big-step
2196:Overview
2074:11621980
1904:27251254
1785:Integers
1652:14735849
1551:Integers
1387:11507540
986:10190144
912:15866917
855:31888376
752:See also
671:software
667:hardware
366:Parallel
336:OR-Tools
269:(CDCL).
180:Overview
2870:Outline
2676:E-graph
2549:Testing
2534:Fuzzing
2509:Dynamic
2474:Pointer
1983:2484208
1912:5528978
1874:Bibcode
1848:7912943
1797:3083419
1791:: A46.
1770:1696473
1571:2684128
1537:7912943
1080:9292941
538:runtime
527:WalkSAT
353:(BDD).
245:is the
66:or not
62:) and (
52:Boolean
2645:Linear
2628:Logics
2464:Escape
2419:Static
2365:Models
2177:
2167:
2111:
2072:
2064:
2023:
1981:
1973:
1910:
1902:
1894:
1866:Nature
1846:
1836:
1795:
1768:
1760:
1697:
1687:
1650:
1640:
1608:
1577:
1569:
1535:
1525:
1479:
1445:
1385:
1375:
1263:
1078:
1068:
1030:
1020:
984:
948:
910:
853:
813:
795:
210:) OR (
164:, and
2834:Twelf
2824:NuPRL
2819:Mizar
2792:Idris
2739:Alloy
2695:Tools
2635:Hoare
2479:Shape
2432:Alias
2319:Types
2175:S2CID
2128:arXiv
2070:S2CID
2001:(PDF)
1979:S2CID
1908:S2CID
1844:S2CID
1816:arXiv
1766:S2CID
1695:S2CID
1669:(PDF)
1648:S2CID
1575:S2CID
1533:S2CID
1505:arXiv
1469:(PDF)
1383:S2CID
1355:arXiv
1284:(PDF)
1121:(PDF)
1098:(PDF)
1076:S2CID
1050:(PDF)
1028:S2CID
1006:(PDF)
982:S2CID
908:S2CID
876:(PDF)
851:S2CID
673:. In
639:FPGAs
629:. In
591:1.307
555:1.308
414:seeds
324:GRASP
320:Chaff
42:is a
2814:LEGO
2809:Lean
2787:HOL4
2767:Agda
2762:ACL2
2744:TLA+
2600:and
2442:kCFA
2165:ISBN
2109:ISSN
2062:ISSN
2021:ISBN
1971:ISSN
1900:PMID
1892:ISSN
1834:ISBN
1758:ISSN
1685:ISBN
1638:ISBN
1606:ISBN
1523:ISBN
1477:ISBN
1443:ISBN
1373:ISBN
1261:ISBN
1066:ISBN
1018:ISBN
946:ISBN
811:ISBN
704:and
669:and
345:and
322:and
292:CDCL
273:DPLL
241:The
206:AND
106:and
86:and
78:and
38:, a
34:and
2829:PVS
2772:Coq
2721:SMT
2716:SAT
2711:CHC
2671:BDD
2157:doi
2101:doi
2097:213
2054:doi
2013:doi
1963:doi
1882:doi
1870:534
1826:doi
1750:doi
1677:doi
1630:doi
1598:doi
1559:doi
1515:doi
1435:doi
1365:doi
1253:doi
1110:doi
1058:doi
1010:doi
974:doi
970:103
936:doi
898:hdl
890:doi
843:doi
803:doi
723:In
716:In
665:of
540:of
494:.
392:or
222:An
58:or
30:In
2897::
2777:F*
2173:.
2163:.
2151:.
2107:.
2095:.
2091:.
2068:.
2060:.
2050:54
2048:.
2044:.
2019:.
2009:58
2007:.
2003:.
1977:.
1969:.
1959:19
1957:.
1953:.
1928:.
1906:.
1898:.
1890:.
1880:.
1868:.
1864:.
1842:,
1832:,
1824:,
1793:MR
1789:12
1787:.
1764:.
1756:.
1746:17
1744:.
1740:.
1693:.
1683:.
1671:.
1646:,
1636:,
1604:,
1573:.
1567:MR
1565:.
1555:10
1553:.
1531:,
1521:,
1513:,
1471:.
1441:,
1418:^
1402:.
1381:,
1371:,
1363:,
1328:.
1304:.
1286:.
1259:,
1239:^
1223:.
1199:.
1175:.
1106:48
1104:.
1100:.
1074:.
1064:.
1052:.
1026:.
1016:.
980:.
968:.
944:,
920:^
906:.
896:.
884:.
878:.
849:.
837:.
819:,
809:,
801:,
748:.
708:.
688:,
326:.
253:.
218:))
190:A
176:.
160:,
156:,
152:,
148:,
137:,
2225:e
2218:t
2211:v
2181:.
2159::
2136:.
2130::
2115:.
2103::
2076:.
2056::
2015::
1985:.
1965::
1938:.
1914:.
1884::
1876::
1828::
1818::
1799:.
1772:.
1752::
1701:.
1679::
1632::
1600::
1581:.
1561::
1517::
1507::
1485:.
1437::
1412:.
1367::
1357::
1338:.
1314:.
1290:.
1255::
1233:.
1209:.
1185:.
1161:.
1130:.
1112::
1082:.
1060::
1034:.
1012::
988:.
976::
938::
914:.
900::
892::
886:5
857:.
845::
839:7
805::
600:)
595:n
587:(
584:O
564:)
559:n
551:(
548:O
451:F
228:v
216:z
212:x
208:y
204:x
202:(
139:y
135:x
92:x
88:y
84:x
80:y
76:x
68:y
64:x
60:y
56:x
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.