BerkMin: A fast and robust SAT-solver

DOI10.1016/j.dam.2006.10.007zbMath1121.68106MaRDI 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

zbMATH Keywords

decision-making procedure; satisfiability testing; clause database management

Mathematics Subject Classification ID

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Related Items

Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution, BerkMin, Logic programming with infinite sets, Answer set programming based on propositional satisfiability, The complexity of pure literal elimination, Symbolic techniques in satisfiability solving, Some computational aspects of DISTANCE SAT, New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability, Dynamic symmetry-breaking for Boolean satisfiability, A generative power-law search tree model, Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems, \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver, Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., A SAT approach to query optimization in mediator systems, On deciding subsumption problems, Bounded model checking of infinite state systems, Satisfiability testing of Boolean combinations of pseudo-Boolean constraints using local-search techniques, The model evolution calculus as a first-order DPLL method, On look-ahead heuristics in disjunctive logic programming, Search techniques for SAT-based Boolean optimization, Visualizing SAT instances and runs of the DPLL algorithm, Solving SAT problem by heuristic polarity decision-making algorithm, Conflict analysis in mixed integer programming, GridSAT: Design and implementation of a computational grid application, Verification of embedded systems based on interval analysis, The state of SAT, BerkMin: A fast and robust SAT-solver, Random backtracking in backtrack search algorithms for satisfiability, A Decision-Making Procedure for Resolution-Based SAT-Solvers, Improvements to Hybrid Incremental SAT Algorithms, Towards Robust CNF Encodings of Cardinality Constraints, Boundary Points and Resolution

Uses Software

• SATO
• Chaff
• CMU Benchmarks
• SATLIB Benchmark Suite
• Velev SAT Benchmarks

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A constraint-based approach to narrow search trees for satisfiability
• BerkMin: A fast and robust SAT-solver
• GRASP: a search algorithm for propositional satisfiability
• SATO: An efficient propositional prover
• A machine program for theorem-proving