Conflict-Driven Clause Learning SAT Solvers

By Joao Marques-Silva, Inês Lynce, Sharad Malik. Handbook of Satisfiability, 2021

636 citations recorded by the source corpus.

One of the most important paradigm shifts in the use of SAT solvers for solving industrial problems has been the introduction of clause learning. Clause learning entails adding a new clause for each conflict during backtrack search. This new clause prevents the same conflict from occurring again during the search process. Moreover, sophisticated techniques such as the identification of unique implication points in a graph of implications, allow creating clauses that more precisely identify the assignments responsible for conflicts. Learned clauses often have a large number of literals. As a result, another paradigm shift has been the development of new data structures, namely lazy data structures, which are particularly effective at handling large clauses. These data structures are called lazy due to being in general unable to provide the actual status of a clause. Efficiency concerns and the use of lazy data structures motivated the introduction of dynamic heuristics that do not require knowing the precise status of clauses. This chapter describes the ingredients of conflict-driven clause learning SAT solvers, namely conflict analysis, lazy data structures, search restarts, conflict-driven heuristics and clause deletion strategies.

Subfields: Artificial Intelligence, Management Information Systems

View Paper: https://www.semanticscholar.org/paper/6899e192961ccf6e36a3d4a703cb1c840414a219

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Management Information Systems

Citations in the corpus

SAT-Based Encodings for Optimal Decision Trees with Explicit Paths (2020, background): “Standard notions and notation for propositional logic are assumed [36].”
Combinatorial optimization and reasoning with graph neural networks (2021, methodology): “In particular, the role of branch-and-bound as the core algorithm is instead taken by Conflict-Driven Clause Learning (CDCL), a tree search algorithm that constructs a solution through a combination of backtracking and learning new clauses from conflicts (Marques-Silva et al., 2021).”
Potassco: The Potsdam Answer Set Solving Collection (2011, neutral): “[15,81]).”
Conflict-driven answer set solving: From theory to practice (2012, methodology): “While the general outline of search is the same as in Conflict-Driven Clause Learning (CDCL; [97,127,23,96]), the state-of-the-art algorithm for industrial SAT solving, the integration of unfounded set checking is particular to ASP and owed to its elevated expressiveness (cf.”
Solving non-linear arithmetic (2012, methodology): “The new procedure performs a backtracking search for a model in R, where the backtracking is powered by a novel con.ict resolution procedure.”
Learning a SAT Solver from Single-Bit Supervision (2018, background): “Modern SAT solvers based on backtracking search are extremely well-engineered and have been able to solve problems of practical interest with millions of variables (Biere et al., 2009).”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, background): “The variable x is known as the Unique Implication Point [101].”
DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (2014, background): “Emitting a DRAT proof from a conﬂict-driven clause-learning (CDCL) [16] solver and preprocessors is relatively easy.”