BerkMin: A fast and robust SAT-solver

By E. Goldberg, Yakov Novikov. Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, 2002

920 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Electrical and Electronic Engineering, Hardware and Architecture

View Paper: https://www.semanticscholar.org/paper/1f74f562a5117cfb2c1bea0bbeae38e213112ca5

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 Electrical and Electronic Engineering

In Hardware and Architecture

Citations in the corpus

DPLL( T): Fast Decision Procedures (2004, background): “(3m) 102 (3m) 18257 (3m) 18438 3601 Two queues (3m) 19.5 (3m) 18019 (3m) 18028 73.6 Benchmark family Hybrid 2 BerkMin Chaff DPLL(T) Buggy Cache 3 3.2 3.7 6.7 Code Validation Suite 27.7 28 28.6 3.7 DLX processor 11.3 12.9 14.3 1.2 Elf processor 47.2 3182 5467 575 Out of order proc.”
Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (2013, methodology): “For instance, the final state of variable ordering [2], polarity cache [17] and clause deletion/restarts strategies [18,14,19] can be easily saved for the next call.”
Handbook of satisfiability (2009, background): “, [52, 33, 22]), highly-engineered data structures and implementation tricks (e.”
Potassco: The Potsdam Answer Set Solving Collection (2011, neutral): “, vsids [84], berkmin [62], and vmtf [90].”
History of Interactive Theorem Proving (2014, methodology): “The formerly neglected area of propositional tautology and satisfiability checking (SAT) underwent a dramatic revival, with systems in the established Davis-Putnam tradition making great strides in efficiency [Moskewicz et al., 2001; Goldberg and Novikov, 2002; Eén and Sörensson, 2003], other algori”
Kodkod: A Relational Model Finder (2007, methodology): “The performance data includes the size of the generated CNF and the time, in seconds, taken to generate and solve it using various SAT engines [41,31,30].”
The Quest for Efficient Boolean Satisfiability Solvers (2002, methodology): “In [21], the authors propose to capture the activity by conflicts.”
PicoSAT Essentials (2008, background): “Other learned clauses are garbage collected in the reduction phase based on their activity as usual [17].”
clasp : A Conflict-Driven Answer Set Solver (2007, methodology): “clasp’s nogood deletion strategy borrows ideas from minisat [17] and berkmin [15].”
Conflict-Driven Answer Set Solving (2007, methodology): “The default restart and nogood deletion policies are adopted from MiniSat [Eén and Sörensson, 2003]; the standard heuristics is an adjustment of BerkMin [Goldberg and Novikov, 2002].”
Software Abstractions - Logic, Language, and Analysis (2006, methodology): “The Alloy Analyzer is bundled with several SAT solvers, the fastest of which are Chaff [55] and Berkmin [19], and a preference setting lets you choose which is used.”
Performing Bayesian Inference by Weighted Model Counting (2005, methodology): “Programs such as zChaff (Zhang et al. 2001) and Berkmin (Goldberg and Novikov 2002) are routinely used in industry and academia to solve difficult problems in hardware verification, planning, scheduling, and experiment design (Kautz and Selman 2003).”
On Solving the Partial MAX-SAT Problem (2006, methodology): “With highly optimized state-of-the-art SAT solvers like zChaff [16], Berkmin [6], Siege [17] and MiniSat [4] , the most straightforward way is to translate the PM-SAT problem directly into a SAT instance.”
Conflict-driven answer set solving: From theory to practice (2012, background): “[72,35]) is an important technique preventing conflict-driven learning solvers from blowing up in space.”