Chaff: engineering an efficient SAT solver

By Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, Sharad Malik. Proceedings - Design Automation Conference, 2001

3,841 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Computer Networks and Communications, Industrial and Manufacturing Engineering

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

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 Computer Networks and Communications

In Industrial and Manufacturing Engineering

Citations in the corpus

A Survey of Automated Techniques for Formal Software Verification (2008, background): “ACKNOWLEDGMENT The authors would like to thank M. Mazzucchi, V. Schuppan, and T. Wahl for their helpful input.”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, background): “Further lines of research examine heuristics for which variable to choose as a decision and what value it should be assigned, and when to restart the SAT search [14, 66, 86, 94].”
Constraint Propagation (2006, positive): “for efficient unit propagation in their Chaff solver for SAT [97].”
Techniques Inspired by Local Search for Incomplete MaxSAT and the Linear Algorithm: Varying Resolution and Solution-Guided Search (2019, background): “Variables are chosen based on their recent activity in conflicts (VSIDS scheme [21]).”
Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (2013, methodology): “So-called “modern SAT solvers” are based on the conflict driven clause learning paradigm (CDCL) [2].”
New Advances in Compiling CNF into Decomposable Negation Normal Form (2004, methodology): “decide( l) succeeds if no contradiction is discovered by unit resolution, otherwise, it will fail after having constructed a conflict–driven clause as described in [10].”
Information-based branching schemes for binary linear mixed integer problems (2009, background): “…(Kılınç Karzan et al. (2008)), Achterberg and Berthold (2009) suggest Hybrid branching, a strategy that combines pseudocosts, inference values, and conflict values (related to the variable independent decaying sum strategy of SAT solvers (Moskewicz et al. (2001))) with clause length information.”
The Algorithm Design Manual (2020, background): “Chaff [MMZ01] is a particularly influential solver, available at http://www.”
Towards Understanding and Harnessing the Potential of Clause Learning (2004, methodology): “Our empirical results are based on our extension of the popular SAT solver zChaff (Moskewicz et al., 2001).”
ASSAT: computing answer sets of a logic program by SAT solvers (2002, neutral): “0,we tried the following SAT solvers: Chaff2 (Mar 23, 2001 version) [17], Walksat 41 [19], GRASP (Feb, 2000 version) [20], Satz 215.”
BerkMin: A fast and robust SAT-solver (2002, methodology): “clauses allows one to prune many of the branches of the search tree that are yet to be examined [1,13,15,18].”
Impact-Based Search Strategies for Constraint Programming (2004, methodology): “In particular it is used in the SAT solver Chaff [14] where variable and value choices at the top of the tree are made randomly until a certain depth.”
SCIP: solving constraint integer programs (2009, methodology): “The hybrid reliability/inference branching rule combines the selection criteria of reliability branching and inference branching, and augments this with the so-called variable state independent decaying sum rule as it is used in SAT solvers based on conflict analysis [84], see [2] for details.”
An Extensible SAT-solver (2003, methodology): “Propagation. The propagation procedure of MINISAT is largely inspired by that of CHAFF [ MZ01 ].”