Cha : Engineering an e cient SAT solver

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

746 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/7b912b3c5bf4609a6f326ed5afdf5f78fd90d0c2

How researchers see this paper

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

Citations in the corpus

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.”
HAMPI: a solver for string constraints (2009, methodology): “Such an approach to analyzing programs is becoming more e ective as the e ciency of o -the-shelf constraint solvers for Boolean SAT [12, 30 ] and other theories [11, 18] continues to increase.”
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 conﬂicts (VSIDS scheme [21]).”
Learning to Solve QBF (2007, background): “While the VSIDS score (Moskewicz et al. 2001) is mainly based on recent conﬂicts occurred during the search, the cube score (Zhang & Malik 2002) is based on the recently encountered solutions.”
Efficient CNF Encoding of Boolean Cardinality Constraints (2003, methodology): “We compared, using some instances of discrete tomography, the performance of our encoding solved by the state of the art SAT solver zchaff [15] versus a commercial constraint solver.”
SAT-Based Model Checking without Unrolling (2011, methodology): “To investigate this question, we selected eight benchmarks from the competition that are diﬃcult but possible for the non-parallel version: Intel benchmarks 20, 21, 22, 23, 24, 29, 31, and 34.”
Bounded synthesis (2007, methodology): “The satisﬁability of the constraint system can be checked using standard SMT solvers [10,14].”
Bounded model checking (2003, methodology): “A recently suggested strategy, called Variable State Independent Decaying Sum (VSIDS) [22], avoids this overhead by ignoring whether the clause is currently satisﬁable or not.”
Computing (2021, unknown): “Thus, the literature highlighted in this chapter, and the case study presented, is focused on furthering how we conceive of affective computing in the context of the built environment.”
Learning action models from plan examples using weighted MAX-SAT (2007, methodology): “We then transform the constraints extracted from the plans into a weighted MAX-SAT representation [25,30,49], solve it and produce action models from the solution of the SAT problem.”
Towards Clause-Learning State Space Search: Learning to Recognize Dead-Ends (2016, background): “The ability to analyze conﬂicts, and to learn clauses that avoid similar mistakes in the future, is a key ingredient to the success of SAT solvers (e. g. (Marques-Silva and Sakallah 1999; Moskewicz et al. 2001; E´en and S¨orensson 2003)).”
PicoSAT Essentials (2008, methodology): “The costs of separate watchers can be avoided by following the suggestion made in [15], which is inspired by the implementation of the original mChaﬀ [28], and implemented in CompSAT [6] and MiniSAT [11].”
Applying SAT Methods in Unbounded Symbolic Model Checking (2002, methodology): “The reader may refer, for example, to [16, 13] for a detailed treatment.”
Translating Pseudo-Boolean Constraints into SAT (2006, background): “Recently, a number of PB-solvers have been formed by extending existing SAT-solvers to support PB-constraints natively , for instance PBS [2], P UEBLO [30], G ALENA [13], and, somewhat less recently, OPBDP [8], which is based on pre-Chaﬀ [24] SAT techniques, but still performs remarkably well.”
Behavioral consistency of C and Verilog programs using bounded model checking (2003, methodology): “In BMC, the transition relation for a complex state machine and its speciﬁcation are jointly unwound to obtain a Boolean formula, which is then checked for satisﬁability by using a SAT procedure such as GRASP [5] or Chaff [6].”
Potassco: The Potsdam Answer Set Solving Collection (2011, unknown): “In the default setting, loop nogoods are created for individual unfounded atoms, as shown in [40]. clasp ’s primary decision heuristics, selectable via option --heuristic , use look-back strategies derived from corresponding CDCL-based approaches in SAT, viz., vsids [84], berkmin [62] and vmtf [90].”
Backdoors to typical case complexity (2003, unknown): “In fact, current state-of-the-art SAT solvers can handle problem instances, as they arise in ﬁnite model-checking and planning, with up to a million variables and ﬁve million clauses [15].”
Planning as satisfiability: Heuristics (2012, background): “What would naturally be a many-valued state variable in higher level languages is often represented as several dependent Boolean variables in PDDL and STRIPS.”
Hybrid Branching (2009, unknown): “The variable state independent decaying sum (VSIDS) [6] branching strategy, which is a common rule in SAT solving, prefers variables that have been used to create recent conﬂict clauses.”