BerkMin: A fast and robust SAT-solver

From MaRDI portal
Publication:2643301

DOI10.1016/j.dam.2006.10.007zbMath1121.68106OpenAlexW2143934828MaRDI QIDQ2643301

Eugene Goldberg, Yakov Novikov

Publication date: 23 August 2007

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.dam.2006.10.007



Related Items

Bounded model checking of infinite state systems, Evaluating CDCL Variable Scoring Schemes, Propositional SAT Solving, Satisfiability testing of Boolean combinations of pseudo-Boolean constraints using local-search techniques, The state of SAT, BerkMin: A fast and robust SAT-solver, Random backtracking in backtrack search algorithms for satisfiability, The model evolution calculus as a first-order DPLL method, Cutting plane versus compact formulations for uncertain (integer) linear programs, Answer set programming based on propositional satisfiability, The complexity of pure literal elimination, Symbolic techniques in satisfiability solving, Application of productions for automatic control of logical design of discrete devices, Some computational aspects of DISTANCE SAT, Formal verification of logical descriptions with functional uncertainty based on logarithmic encoding of conditions, Parallel Logic Programming: A Sequel, Decomposition representations of logical equations in problems of inversion of discrete functions, A Decision-Making Procedure for Resolution-Based SAT-Solvers, Improvements to Hybrid Incremental SAT Algorithms, Towards NP-P via proof complexity and search, On look-ahead heuristics in disjunctive logic programming, A taxonomy of exact methods for partial Max-SAT, Dealing with satisfiability and \(n\)-ary CSPs in a logical framework, Towards Robust CNF Encodings of Cardinality Constraints, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Advancing Lazy-Grounding ASP Solving Techniques – Restarts, Phase Saving, Heuristics, and More, Search techniques for SAT-based Boolean optimization, New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability, An overview of parallel SAT solving, Visualizing SAT instances and runs of the DPLL algorithm, DPLL: The Core of Modern Satisfiability Solvers, Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One, Solving SAT problem by heuristic polarity decision-making algorithm, Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models, Conflict analysis in mixed integer programming, Conflict-driven ASP solving with external sources, An interleaved depth-first search method for the linear optimization problem with disjunctive constraints, Producing and verifying extremely large propositional refutations, Efficient branch-and-bound algorithms for weighted MAX-2-SAT, Conflict-driven answer set solving: from theory to practice, On the power of clause-learning SAT solvers as resolution engines, Dynamic symmetry-breaking for Boolean satisfiability, A SAT approach to query optimization in mediator systems, On deciding subsumption problems, GridSAT: Design and implementation of a computational grid application, Verification of embedded systems based on interval analysis, A generative power-law search tree model, Learning Rate Based Branching Heuristic for SAT Solvers, BerkMin, Boundary Points and Resolution, Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution, Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems, \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver, Bounded Model Checking with Parametric Data Structures, Interpolant Learning and Reuse in SAT-Based Model Checking, Logic programming with infinite sets, Deep cooperation of CDCL and local search for SAT


Uses Software


Cites Work