GRASP: A Search Algorithm for Propositional Satisfiability

By Joao Marques-Silva, Karem A. Sakallah. 1999

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

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, methodology): “This is a particular case of conflict analysis, which is a standard technique in SAT and SMT solvers [25].”
The SCIP Optimization Suite 7.0 (2020, background): “In that case, conﬂict analysis is not directly applicable because so far conﬂict graph and dual proof analysis rely on globally valid proofs, see, e.g., [63, 1, 77].”
Information-based branching schemes for binary linear mixed integer problems (2009, background): “The concepts of learning and restarts have been used in artificial intelligence to solve, for example, satisfiability (SAT) problems (see [24,32]).”
Lazy proofs for DPLL(T)-based SMT solvers (2016, methodology): “In particular, Confl and Expl model the conflict discovery and analysis mechanism used by CDCL SAT solvers [18].”
On Solving the Partial MAX-SAT Problem (2006, methodology): “But unfortunately, Scherzo is not able to solve any of the benchmarks in the following tables. bsolo is another state-of-the-art branch-and-bound BCP/UCP solver based on the SAT solver GRASP [14]. cplex is the cutting edge commercial Linear Programming (LP) solver that is also capable of finding int”
Chaff: engineering an efficient SAT solver (2001, methodology): “GRASP [8], POSIT [5], SATO [13], rel_sat [2], WalkSAT [9]) have been developed, most employing some combination of two main strategies: the Davis-Putnam (DP) backtrack search and heuristic local search.”
Branch-and-bound algorithms: A survey of recent advances in searching, branching, and pruning (2016, unknown): “Marques-Silva and Sakallah [130] present a SAT solver that makes use of this technique.”
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.”
BerkMin: A fast and robust SAT-solver (2002, methodology): “BerkMin uses the procedures of conflict analysis and non-chronological backtracking introduced in GRASP, fast BCP suggested in SATO, and Chaff s idea of reducing the contribution of aged conflict clauses into decision making.”
Simplify: a theorem prover for program checking (2005, methodology): “Compared to recent advances in propositional SAT solving [Zhang 1997; Guerra e Silva et al. 1999; Silva and Sakallah 1999; Moskewicz et al. 2001], the backtracking search described in this section is simple and old-fashioned.”