Constraint satisfaction, SAT solvers and SMT solvers

Constraint satisfaction is the symbolic AI method of stating a problem as variables, the values each may take, and constraints that combinations of values must obey, then searching for an assignment that satisfies every constraint. A SAT solver does this for true/false variables; an SMT solver adds arithmetic, arrays and other theories.

1. Constraint satisfaction problems and how they are solved

1.1 Constraint satisfaction problems (CSP)

A constraint satisfaction problem is a triple of variables, domains and constraints. The formulation grew out of early 1970s work on scene analysis: David Waltz’s MIT thesis (1972, published 1975) labelled the lines of drawings of three-dimensional scenes by repeatedly deleting labels that no neighbouring junction could accept [3], and Ugo Montanari’s 1974 “Networks of constraints” gave the general algebraic treatment [2].

The standard teaching example is colouring the map of Australia so that no two neighbouring regions share a colour [1]. The variables are the seven regions WA, NT, SA, Q, NSW, V and T; every domain is {red, green, blue}; and there is one constraint $A\ne B$ for each shared border (WA–NT, WA–SA, NT–SA, NT–Q, SA–Q, SA–NSW, SA–V, Q–NSW, NSW–V). One solution is WA = red, NT = green, SA = blue, Q = red, NSW = green, V = red, T = red. Sudoku, timetabling, staff rostering, product configuration and the eight-queens puzzle have exactly the same shape. The point of the formalism is separation: the modeller writes what must hold, and a general solver decides how to find it.

Limits. Deciding whether a CSP with finite domains has a solution is NP-complete in general (map colouring with three colours already is), so every complete solver takes exponential time on some inputs. Plain CSPs also have no notion of “better”: preferences need an extension such as constraint optimisation or weighted constraints.

1.2 Backtracking search

Backtracking is the basic complete algorithm. Assign variables one at a time; after each assignment check the constraints whose variables are all assigned; on a violation, undo the most recent choice and try the next value. Solomon Golomb and Leonard Baumert named and analysed the method in “Backtrack Programming” (Journal of the ACM, 1965) [6]. Its worst case is the full product of the domains, ${\prod }_{i=1}^n\left|D_i\right|$, so practical solvers add three kinds of intelligence:

• Variable ordering. Pick the variable with the fewest remaining values (“minimum remaining values”, or fail-first), breaking ties by the most constraints on unassigned variables. On the Australia map, after WA = red, both NT and SA are down to two colours; choosing SA next (it touches five regions) exposes contradictions earliest.
• Value ordering. Try the value that rules out the fewest options for the neighbours first.
• Look-ahead. Robert Haralick and Gordon Elliott’s forward checking (1980) deletes, after each assignment, every value of each unassigned neighbour that conflicts with it, so a dead end is noticed as soon as some domain becomes empty rather than when that variable is reached. Their paper states the two principles every later solver follows: try first where failure is most likely, and remember what has been done to avoid repeating the same mistake [7].

Today. Every constraint programming solver is still a backtracking search at heart, wrapped around propagation (§1.4). Limits. Chronological backtracking returns to the most recent choice even when an earlier one caused the failure, which is the thrashing that conflict analysis in SAT solvers (§2.3) was built to avoid.

1.3 Arc consistency and AC-3

Arc consistency is the most used form of local consistency: a cheap test that removes values which cannot be part of any solution, before or during search. Alan Mackworth’s 1977 paper “Consistency in networks of relations” defined node, arc and path consistency as a unified family and gave the AC-3 algorithm [4].

AC-3 keeps a queue of arcs. It removes each arc in turn and calls REVISE, which deletes every $a$ in $D_i$ that has no support; whenever $D_i$ shrinks, every arc $(x_k,x_i)$ pointing into $x_i$ goes back on the queue, because its supports may have disappeared. If a domain becomes empty, the problem has no solution.

Every domain is now a single value, and A = 1, B = 2, C = 3 is the solution without any guessing. On harder problems arc consistency only prunes, and search does the rest. With $e$ binary constraints and domains of size at most $d$, AC-3 runs in $O\left(e{d}^3\right)$ time, as Mackworth and Eugene Freuder showed in 1985 [5]; later algorithms (AC-4 onward) reduce this to $O\left(e{d}^2\right)$. Limits. Arc consistency is local: a problem can be arc consistent and still have no solution (three variables, each with domain {red, green}, pairwise different, is arc consistent and unsolvable).

1.4 Constraint propagation

Constraint propagation is the general idea behind §1.3: use each constraint to shrink the domains of its variables, and let every reduction trigger the constraints that share those variables, until nothing changes (a fixed point) or a domain empties. Stronger levels of consistency trade more work for more pruning. Montanari (1974) introduced path consistency, which reasons about triples of variables [2]; Freuder (1978) generalised the ladder to k-consistency and showed how enough consistency makes search backtrack-free [8].

The most useful step in practice was the global constraint: a constraint over many variables with its own specialised propagator. alldifferent(x1, …, xn) is the classic. Posting it as $n(n-1)/2$ separate inequalities misses the pigeonhole argument that three variables cannot share two values; Jean-Charles Régin’s 1994 filtering algorithm uses bipartite matching to remove every value that cannot appear in any all-different assignment [9]. Global constraints for scheduling (cumulative resources), routing and packing are why constraint programming is competitive on industrial scheduling. Limits. Propagation is incomplete by design; it narrows the search, it does not replace it, and choosing how much propagation to pay for is still an empirical question.

1.5 Local search: min-conflicts, GSAT and WalkSAT

Complete search proves things; local search just tries to find a solution fast. Start from a full assignment that violates some constraints and repeatedly change one variable to reduce the number of violations. Steven Minton, Mark Johnston, Andrew Philips and Philip Laird’s min-conflicts heuristic (AAAI-90) came from scheduling Hubble Space Telescope observations and solves the million-queens problem in about 50 repairs from a good starting assignment [10]. For SAT, Bart Selman, Hector Levesque and David Mitchell’s GSAT (1992) flips the variable that satisfies the most clauses [16], and WalkSAT (Selman, Henry Kautz and Bram Cohen) adds random “noise” moves to escape local minima. Limits. Local search is incomplete: it can find a solution, but if none exists it never says so. It cannot prove unsatisfiability, which is exactly the answer a verifier needs.

1.6 Constraint logic programming

Constraint logic programming (CLP) puts constraint solving inside a logic programming language. Joxan Jaffar and Jean-Louis Lassez’s CLP(X) scheme (POPL 1987) generalised features that Alain Colmerauer had introduced in Prolog II: a Prolog-like language parameterised by a constraint domain X, where some atoms are ordinary clauses and others are constraints handed to a solver [11]. CHIP, developed at the European Computer-Industry Research Centre (ECRC) by Mehmet Dincbas, Pascal Van Hentenryck and colleagues and described in 1988, was the first to implement constraint programming over finite domains, CLP(FD), and introduced global constraints [12].

A small CLP(FD) program for the A < B < C problem above reads almost like its specification:

solve([A,B,C]) :-
    [A,B,C] ins 1..3,     % domains
    A #< B, B #< C,       % constraints: propagated as they are posted
    label([A,B,C]).       % search whatever propagation left open

Today. SWI-Prolog, SICStus Prolog and ECLiPSe ship finite-domain constraint libraries, and the solver-independent modelling language MiniZinc (Nethercote, Stuckey and colleagues, 2007) lets one model run on many constraint, MIP and SAT back ends [13]. CLP connects this page to logic programming and theorem proving. Limits. Performance depends heavily on how the model is written, which is a craft; two logically equivalent models can differ by orders of magnitude.

2. SAT: Boolean satisfiability and SAT solvers

2.1 The SAT problem

Boolean satisfiability (SAT) is the CSP whose variables are true/false. Formulas are usually given in conjunctive normal form (CNF): an AND of clauses, each an OR of literals (a variable or its negation). The question is whether some assignment makes every clause true. SAT was the first problem proved NP-complete, by Stephen Cook in 1971 and independently by Leonid Levin [14]; Richard Karp’s 1972 list of 21 NP-complete problems started from it. So every problem in NP can be translated into SAT, which is why a fast SAT solver is a general-purpose tool: planning, scheduling, hardware equivalence and package dependencies can all be encoded as clauses. Special cases are easy: 2-SAT (two literals per clause) is solvable in polynomial time, and Horn clauses by unit propagation alone.

On randomly generated 3-SAT formulas, difficulty peaks sharply near a ratio of about 4.26 clauses per variable, where formulas pass from almost always satisfiable to almost always unsatisfiable [17]. Industrial formulas, by contrast, have structure that modern solvers exploit, which is why they routinely solve instances far larger than any random formula they could.

2.2 DPLL

Martin Davis and Hilary Putnam published a procedure for testing satisfiability in 1960, as part of a proof method for first-order logic [15]. Its variable-elimination step used too much memory, and in 1962 Davis, George Logemann and Donald Loveland replaced it with splitting and backtracking [18]. The result, called DPLL, is still the skeleton of complete SAT solvers. It repeats three steps:

1. Unit propagation. If a clause has all its literals false except one unassigned literal, that literal must be true. Assign it, and repeat; this is the SAT form of constraint propagation.
2. Pure literal elimination. If a variable appears with only one sign, set it to satisfy those clauses.
3. Split. Otherwise choose an unassigned variable, try one value, and recurse; if that leads to an empty (all-false) clause, backtrack and try the other value.

A worked trace on six clauses over five variables:

Anyone can check the model in one pass over the clauses; that asymmetry between finding and checking is the practical meaning of NP. Limits. Plain DPLL backtracks chronologically and forgets why a branch failed, so it can rediscover the same contradiction in many parts of the search tree.

2.3 Conflict-driven clause learning (CDCL)

Conflict-driven clause learning fixes DPLL’s amnesia. When propagation hits a conflict, the solver analyses why, writes the reason down as a new clause, and jumps back to the decision that actually caused it. João Marques-Silva and Karem Sakallah introduced it in the GRASP solver (ICCAD 1996; IEEE Transactions on Computers, 1999) [19], with related look-back work by Roberto Bayardo and Robert Schrag (1997) [20]. Chaff (Moskewicz, Madigan, Zhao, Zhang and Malik, DAC 2001) made it fast: two watched literals per clause make unit propagation cheap, and the VSIDS heuristic branches on variables that appear in recent conflicts [21]. MiniSat (Niklas Eén and Niklas Sörensson, 2003) packaged the design in a small, readable solver that became the standard base for research [22]. Restarts, which abandon the current branch but keep the learned clauses, complete the modern recipe.

On the trace above, the conflict at step 4 came from the decision $a$ through $c_2$, $c_4$ and $c_3$. Conflict analysis resolves the falsified clause with the reasons for its literals, in reverse order of propagation:

The learned clause $(\neg a)$ is a consequence of $F$: whatever else happens, $a$ must be false. A CDCL solver adds it, backjumps to level 0 and propagates $a=0$ as a fact, so it never explores $a=1$ again in any branch. Figure 1 shows the implication graph the analysis walks.

Today. Essentially every competitive complete SAT solver (MiniSat descendants, CaDiCaL, Kissat and others) is CDCL, and so is the Boolean core of every SMT solver. Limits. Heuristics such as VSIDS and restart policies are tuned empirically, so performance on a new family of formulas is hard to predict; and there are formulas, such as pigeonhole encodings, on which any resolution-based method, CDCL included, needs exponential time.

3. SMT solvers

3.1 Satisfiability modulo theories (SMT)

Satisfiability modulo theories asks the SAT question for formulas whose atoms belong to a background theory: linear integer or real arithmetic, bit-vectors (machine integers), arrays, uninterpreted functions, strings. Two ideas made it practical. Greg Nelson and Derek Oppen (1979) showed how to combine decision procedures for separate theories by exchanging equalities between shared variables [23]. The DPLL(T) architecture, formalised by Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli (Journal of the ACM, 2006), lets a CDCL SAT solver handle the Boolean structure while a theory solver checks whether the chosen atoms are consistent and, when they are not, returns an explanation that becomes a learned clause [24].

A worked example over the integers:

1. The SAT solver sees only the Boolean skeleton on the right and proposes $p_1,p_2,p_3$.
2. The arithmetic solver checks $x+y>10$, $x\le 2$, $y\le 7$: the last two give $x+y\le 9$, a contradiction. It returns the explanation, and the SAT solver learns $\neg p_1\vee \neg p_2\vee \neg p_3$.
3. Unit propagation now forces $\neg p_3$ and hence $p_4$. The theory solver finds $x<3$ and $x>5$ inconsistent, and the SAT solver learns $\neg p_2\vee \neg p_4$.
4. With $p_1$ and $p_2$ required, the two learned clauses rule out both $p_3$ and $p_4$, so the clause $p_3\vee p_4$ is false: unsatisfiable. Drop the constraint $x<3$ and the solver instead returns a model such as $x=6,y=5$.

Solvers and standards. Z3, from Leonardo de Moura and Nikolaj Bjørner at Microsoft Research (TACAS 2008), is the most widely used [25]; cvc5 (2022), the successor of CVC4, is another major open-source solver [26]; Yices, MathSAT and Bitwuzla are others. The SMT-LIB initiative, running since 2003, defines a common input language and benchmark library, so the same problem can be sent to any of them. Today. SMT solvers are the reasoning engine inside program verifiers such as Dafny (which discharges its proof obligations to Z3), symbolic-execution tools such as KLEE, and bounded model checkers; see formal verification and program synthesis. Limits. Once quantifiers or nonlinear integer arithmetic appear, satisfiability becomes undecidable, and solvers fall back on heuristics that may answer “unknown” or time out.

4. Where constraint, SAT and SMT solvers are used today

• Scheduling, timetabling and rostering. Constraint programming and local search build schedules with many hard rules (no double booking, rest times, capacities) and soft preferences. Min-conflicts began as Hubble Space Telescope scheduling [10].
• Hardware verification. Bounded model checking (Biere, Cimatti, Clarke and Zhu, 1999) unrolls a circuit for $k$ steps and asks a SAT solver whether a bad state is reachable [27]; SAT-based equivalence checking confirms that an optimised circuit still computes the same function.
• Software verification and testing. Verifiers such as Dafny and symbolic-execution engines such as KLEE turn program paths into formulas and ask an SMT solver whether an assertion can fail; a satisfying assignment is a concrete failing input.
• Cloud security policies. Amazon Web Services translates access-control policies into SMT formulas and uses solvers to answer questions such as “can anyone outside the account read this bucket?” (the Zelkova system, FMCAD 2018) [28].
• Package managers. Deciding whether a set of packages can be installed together is NP-complete, as the EDOS project showed for Debian-style dependencies in 2006 [29]. openSUSE’s zypper and Fedora’s DNF resolve dependencies with libsolv, a SAT-based solver, and conda switched its default to the libsolv-based libmamba solver in version 23.10 (2023), replacing a solver built on the PicoSAT SAT solver [30].
• Planning. SATPlan-style planners encode “is there a plan of length $k$?” as a SAT formula; see AI planning.
• Mathematics. In 2016 Marijn Heule, Oliver Kullmann and Victor Marek used a SAT solver to show that the numbers 1 to 7825 cannot be split into two parts without one part containing a Pythagorean triple (while 1 to 7824 can), and verified the result with a DRAT proof of almost 200 terabytes [31].

5. Timeline

6. Strengths and limits

7. Solvers and fail-safe models

A fail-safe model is an AI model built so that its failures end in a controlled, safe state: it abstains when the evidence is missing, and learning can narrow what it does but never widen what it is authorised to do. SAT and SMT solvers show the engineering pattern that makes this possible at small scale. The solver is a large, heavily optimised and therefore fallible program; its answers are not trusted because of it. A claimed solution is checked against the constraints directly, and a claimed “unsatisfiable” can be backed by a clausal proof that a small checker such as DRAT-trim verifies independently [32]. A solver that runs out of time returns “unknown”, and a well-built system treats that as unknown, not as yes.

The same division of labour applies when a language model sits in front of a symbolic layer: a model may propose; only the floor admits a fact. The honest limit carries over as well. A solver certifies the formula it was given; if the encoding of the real-world question is wrong, the certificate is worthless. Checking does not make a system right; it makes its failures end in “not proven” rather than in a confident error. Our paper The Orchestration Gap argues why chain-level invariants need such a layer. Peel, a research prototype by Perslis Research, is built on this principle; to our knowledge it is the first fail-safe model (the exact claim and the closest earlier work are on What is a fail-safe model?). There is no neural network in the loop that decides, and its knowledge is typed, sourced cards.

For the other families of techniques, see the guide to symbolic AI techniques; for how solvers fit into the longer story, the history of symbolic AI.

8. Questions

What is a constraint satisfaction problem?

A constraint satisfaction problem is a set of variables, a domain of possible values for each, and constraints that restrict which combinations of values are allowed. A solution assigns a value to every variable so that every constraint holds. Map colouring, Sudoku, timetabling and product configuration are standard examples.

What is a SAT solver?

A SAT solver is a program that decides whether a Boolean formula, usually written as clauses in conjunctive normal form, can be made true. If it can, the solver returns a satisfying assignment; if not, it reports unsatisfiable and many solvers can also output a proof of that.

What is an SMT solver?

An SMT solver decides satisfiability modulo theories: it handles formulas that mix Boolean logic with arithmetic, bit-vectors, arrays and other theories. It combines a CDCL SAT solver for the logical structure with specialised theory solvers. Z3 and cvc5 are widely used examples.

What is the difference between DPLL and CDCL?

DPLL, from 1962, searches by unit propagation, splitting on a variable and chronological backtracking. CDCL, introduced in the GRASP solver in 1996, adds conflict analysis: each conflict produces a learned clause that prevents the same mistake elsewhere, and the solver jumps back directly to the decision that caused the conflict.

What is arc consistency?

An arc between two variables is consistent when every value in the first variable's domain has at least one compatible value in the second variable's domain. The AC-3 algorithm, published by Alan Mackworth in 1977, deletes unsupported values until every arc is consistent or some domain becomes empty.

Why is SAT important if it is NP-complete?

NP-completeness means no known algorithm is fast on every formula, but real formulas from hardware, software and planning have structure that clause learning exploits. Modern solvers routinely decide industrial instances with millions of clauses, and because every problem in NP can be translated into SAT, one good solver serves many applications.

Are SAT and SMT solvers artificial intelligence?

Yes, in the symbolic sense. They grew out of automated theorem proving and constraint satisfaction research in AI, and they reason exactly over explicit logical constraints. Unlike machine learning models they do not learn from data, and their answers can be checked independently.

Where are SAT and SMT solvers used today?

They are used in hardware and software verification, test generation, scheduling and timetabling, automated planning, cloud access-policy analysis, package dependency resolution in tools such as DNF, zypper and conda, and in mathematics, for example the 2016 solution of the Boolean Pythagorean triples problem.

9. References

1. S. Russell, P. Norvig. Artificial Intelligence: A Modern Approach, 4th ed. Pearson, 2020. (Chapter on constraint satisfaction problems.)
2. U. Montanari. Networks of Constraints: Fundamental Properties and Applications to Picture Processing. Information Sciences 7:95–132, 1974. doi:10.1016/0020-0255(74)90008-5
3. D. Waltz. Understanding Line Drawings of Scenes with Shadows. In P. H. Winston (ed.), The Psychology of Computer Vision. McGraw-Hill, 1975.
4. A. K. Mackworth. Consistency in Networks of Relations. Artificial Intelligence 8(1):99–118, 1977. doi:10.1016/0004-3702(77)90007-8
5. A. K. Mackworth, E. C. Freuder. The Complexity of Some Polynomial Network Consistency Algorithms for Constraint Satisfaction Problems. Artificial Intelligence 25(1):65–74, 1985. doi:10.1016/0004-3702(85)90041-4
6. S. W. Golomb, L. D. Baumert. Backtrack Programming. Journal of the ACM 12(4):516–524, 1965. doi:10.1145/321296.321300
7. R. M. Haralick, G. L. Elliott. Increasing Tree Search Efficiency for Constraint Satisfaction Problems. Artificial Intelligence 14:263–313, 1980.
8. E. C. Freuder. Synthesizing Constraint Expressions. Communications of the ACM 21(11):958–966, 1978. doi:10.1145/359642.359654
9. J.-C. Régin. A Filtering Algorithm for Constraints of Difference in CSPs. Proceedings of AAAI-94, 1994.
10. S. Minton, M. D. Johnston, A. B. Philips, P. Laird. Solving Large-Scale Constraint Satisfaction and Scheduling Problems Using a Heuristic Repair Method. Proceedings of AAAI-90, 17–24, 1990.
11. J. Jaffar, J.-L. Lassez. Constraint Logic Programming. Proceedings of the 14th ACM Symposium on Principles of Programming Languages (POPL), 1987. doi:10.1145/41625.41635
12. M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, T. Graf, F. Berthier. The Constraint Logic Programming Language CHIP. Proceedings of FGCS-88, Tokyo, 1988.
13. N. Nethercote, P. J. Stuckey, R. Becket, S. Brand, G. J. Duck, G. Tack. MiniZinc: Towards a Standard CP Modelling Language. Principles and Practice of Constraint Programming (CP), 2007.
14. S. A. Cook. The Complexity of Theorem-Proving Procedures. Proceedings of the 3rd ACM Symposium on Theory of Computing (STOC), 151–158, 1971. doi:10.1145/800157.805047
15. M. Davis, H. Putnam. A Computing Procedure for Quantification Theory. Journal of the ACM 7(3):201–215, 1960. doi:10.1145/321033.321034
16. B. Selman, H. Levesque, D. Mitchell. A New Method for Solving Hard Satisfiability Problems. Proceedings of AAAI-92, 1992.
17. B. Selman, D. G. Mitchell, H. J. Levesque. Generating Hard Satisfiability Problems. Artificial Intelligence 81(1–2):17–29, 1996. doi:10.1016/0004-3702(95)00045-3
18. M. Davis, G. Logemann, D. Loveland. A Machine Program for Theorem-Proving. Communications of the ACM 5(7):394–397, 1962. doi:10.1145/368273.368557
19. J. P. Marques-Silva, K. A. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers 48(5):506–521, 1999. First presented at ICCAD 1996.
20. R. J. Bayardo, R. C. Schrag. Using CSP Look-Back Techniques to Solve Real-World SAT Instances. Proceedings of AAAI-97, 1997.
21. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. Proceedings of the 38th Design Automation Conference (DAC), 530–535, 2001. doi:10.1145/378239.379017
22. N. Eén, N. Sörensson. An Extensible SAT-solver. SAT 2003, LNCS 2919, 502–518, 2004. doi:10.1007/978-3-540-24605-3_37
23. G. Nelson, D. C. Oppen. Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2):245–257, 1979. doi:10.1145/357073.357079
24. R. Nieuwenhuis, A. Oliveras, C. Tinelli. Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T). Journal of the ACM 53(6):937–977, 2006. doi:10.1145/1217856.1217859
25. L. de Moura, N. Bjørner. Z3: An Efficient SMT Solver. TACAS 2008, LNCS 4963. doi:10.1007/978-3-540-78800-3_24
26. H. Barbosa, C. Barrett, M. Brain, et al. cvc5: A Versatile and Industrial-Strength SMT Solver. TACAS 2022, 415–442. doi:10.1007/978-3-030-99524-9_24
27. A. Biere, A. Cimatti, E. Clarke, Y. Zhu. Symbolic Model Checking without BDDs. TACAS 1999, 193–207. doi:10.1007/3-540-49059-0_14
28. J. Backes, P. Bolignano, B. Cook, C. Dodge, A. Gacek, K. Luckow, N. Rungta, O. Tkachuk, C. Varming. Semantic-based Automated Reasoning for AWS Access Policies using SMT. FMCAD 2018. doi:10.23919/FMCAD.2018.8602994
29. F. Mancinelli, J. Boender, R. Di Cosmo, J. Vouillon, B. Durak, X. Leroy, R. Treinen. Managing the Complexity of Large Free and Open Source Package-Based Software Distributions. ASE 2006, 199–208. doi:10.1109/ASE.2006.49
30. conda project. Conda 23.10.0 release: libmamba is now the default solver. conda.org blog, 6 November 2023. conda.org
31. M. J. H. Heule, O. Kullmann, V. W. Marek. Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer. SAT 2016. arXiv:1605.00723
32. N. Wetzler, M. J. H. Heule, W. A. Hunt Jr. DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs. SAT 2014, 422–429. doi:10.1007/978-3-319-09284-3_31