Efficient conflict driven learning in a Boolean satisfiability solver

By Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, Sharad Malik. IEEE/ACM International Conference on Computer Aided Design. ICCAD 2001. IEEE/ACM Digest of Technical Papers (Cat. No.01CH37281), 2001

898 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Molecular Biology, Software

View Paper: https://www.semanticscholar.org/paper/aedea7a426a42d38ebad02ccbcfbd40fa8dba82a

How researchers see this paper

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

In Computational Theory and Mathematics

In Molecular Biology

In Software

Citations in the corpus

Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (2013, methodology): “If they were initially introduced as an extension of the DPLL algorithm [15], with a powerful conflict clause learning [3,16] scheme, it is acknowledged that they must be described as a mix between backtrack search and plain resolution engines.”
Core-Boosted Linear Search for Incomplete MaxSAT (2019, background): “Modern MaxSAT solving technology builds on the exceptional performance improvements of SAT solvers, starting in the late 90s [39, 49].”
Leakage current reduction in CMOS VLSI circuits by input vector control (2004, background): “In MTCMOS, a high threshold device is inserted in the series with low threshold transistors creating a sleep transistor.”
Handbook of Satisfiability (2021, methodology): “3 shows an online T -DPLL procedure based on a modern DPLL engine [157, 158].”
Towards Understanding and Harnessing the Potential of Clause Learning (2004, methodology): “Our sequence generators work for the 1UIP learning scheme (Zhang et al., 2001), which is one of the best known.”
Performing Bayesian Inference by Weighted Model Counting (2005, methodology): “To provide an optimized implementation of weighted model counting, we have modified Cachet, the fastest exact model-counting system available, which is built on top of zChaff (Zhang et al. 2001).”
The Quest for Efficient Boolean Satisfiability Solvers (2002, background): “In [39], the authors discussed a scheme called the FirstUIP scheme.”
Answer Set Solving in Practice (2012, neutral): “[74] L.”
Predicting Learnt Clauses Quality in Modern SAT Solvers (2009, methodology): “” [Zhang and Madigan, 2001].”
FlashMeta: a framework for inductive program synthesis (2015, methodology): “We were inspired by the success of conflict-driven clause learning in SAT solving [39].”
ManySAT: a Parallel SAT Solver (2009, neutral): “In addition to the classical first-UIP scheme [40], it incorporates a new technique which extends the implication graph used during conflict-analysis to exploit the satisfied clauses of a formula [1].”