An Extensible SAT-solver

By Niklas Eén, Niklas Sörensson. International Conference on Theory and Applications of Satisfiability Testing, 2003

3,398 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/3ccba505e7e719bd9dd3bf83cca7497d29ffb87c

How researchers see this paper

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

In Artificial Intelligence

In Computational Theory and Mathematics

In Computer Networks and Communications

Citations in the corpus

Multi-shot ASP solving with clingo (2017, methodology): “Pioneering work was done in minisat (Eén and Sörensson 2004), furnishing a C++ interface for solving under assumptions.”
PicoSAT Essentials (2008, methodology): “Note that these numbers are calculated after clause minimization [1], as implemented in MiniSAT [11].”
Iterative and core-guided MaxSAT solving: A survey and assessment (2013, background): “In both cases, the aim is to take advantage of modern SAT solvers with powerful clause learning and backjumping techniques [110, 86, 40].”
Solving MAXSAT by Decoupling Optimization and Satisfaction (2014, methodology): “We modi ed the SAT solver minisat (Eén and Sörensson, 2003) to perform a Branch and Bound search for maxsat.”
Translating Pseudo-Boolean Constraints into SAT (2006, background): “Those extra variables might occur among the learned clauses [15] of the SAT-solver, and removing the original clauses containing those variables will vastly reduce the pruning power of the learned clauses.”
History of Interactive Theorem Proving (2014, methodology): “…with systems in the established Davis-Putnam tradition making great strides in efficiency [Moskewicz et al., 2001; Goldberg and Novikov, 2002; Eén and Sörensson, 2003], other algorithms being developed [Bryant, 1986; St̊almarck and Säflund, 1990], and applications to new and sometimes…”
The nuXmv Symbolic Model Checker (2014, methodology): “In this view, NUSMV is the code-base that provides basic functionalities and common data structures to all the other tools (e.g. symbol table, handling of expressions, interface with the CUDD [2] BDD package, interface with the SAT solvers (e.g. MINISAT [3]).”
Constraint-based causal discovery from multiple interventions over overlapping variable sets (2014, methodology): “Hauser and Bühlmann (2012) extend the notion of Markov equivalence for DAGs to the case of interventional distributions arising from multiple experiments, and propose a learning algorithm. Tong and Koller (2001) and Murphy (2001) use Bayesian network theory to propose experiments that are most infor”
Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure (2006, methodology): “In recent years a lot of developments in creating powerful SAT algorithms have been made, leading to state-of-the-art approaches like BerkMin [14], MiniSat [ 10 ], MiraXT [18], and zCha [21].”
Feature Models, Grammars, and Propositional Formulas (2005, background): “The root production is an exception; it is not referenced in any pattern.”
PySAT: A Python Toolkit for Prototyping with SAT Oracles (2018, background): “2 [13, 29] and its GitHub version [30], and also Glucose 3 and Glucose 4.”
Open-WBO: A Modular MaxSAT Solver, (2014, methodology): “With the exception of MINISAT, all other solvers use the LBD measure.”
Efficient Benchmarking of Algorithm Configuration Procedures via Model-Based Surrogates (2017, methodology): “MiniSATHack-K3 is our last benchmark from the CSSC’14; it is based on a modification of the well-known MiniSAT solver (Eén and Sörensson 2003), called Minisat-HACK-999ED (Oh 2014) on 3SAT random instances.”
Discovering Cyclic Causal Models with Latent Variables: A General SAT-Based Procedure (2013, methodology): “The most eﬃcient SAT solvers are based on the complete conﬂict-driven clause learning (CDCL) search algo-rithm (Marques-Silva and Sakallah, 1999; Moskewicz et al., 2001; E´en and S¨orensson, 2004).”
Hydra-MIP : Automated Algorithm Configuration and Selection for Mixed Integer Programming (2011, background): “2 The closest to a SAT equivalent of what CPLEX is for MIP would be MiniSAT [5], but it does not expose many parameters and does not perform well for random instances.”
Improving the Effectiveness of SAT-Based Preprocessing for MaxSAT (2015, methodology): “MiniSAT 2.2.0 [Eén and Sörensson, 2003] is used as the underlying SAT solver and IBM CPLEX 12.6.0 [Cpl, 2015] is used to solve the minimum-cost hitting set IPs.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, methodology): “It further leverages the full power of cvc5 ’s Equality Engine for reasoning about equalities over bit-vector terms and also uses the solve-under-assumptions feature [57] supported by many state-of-the-art SAT solvers.”