Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases

DOI10.1007/978-3-642-15274-0_26MaRDI QIDQ3587716zbMATH OpenOpenAlexFDO

Authors Christoph Zengler, Wolfgang Küchlin

Publication date 10 September 2010

Published in Computer Algebra in Scientific Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-15274-0_26

zbMATH Keywords

MiniSATRedlog

Mathematics Subject Classification ID

Computational learning theory (68Q32) Symbolic computation and algebraic computation (68W30)

Recommendations

• Incorporating clause learning in grid-based randomized SAT solving
• On the power of clause-learning SAT solvers as resolution engines
• Boolean Gröbner bases in SAT solving
• Boosting branch-and-bound MaxSAT solvers with clause learning
• Theory and Applications of Satisfiability Testing
• Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning

Cites work

• A Gröbner Basis Approach to CNF-Formulae Preprocessing
• A machine program for theorem-proving
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Boolean Rings for Intersection-Based Satisfiability
• Bounded model checking using satisfiability solving
• Combining preorder and postorder resolution in a satisfiability solver
• Efficiently Calculating Evolutionary Tree Measures Using SAT
• scientific article; zbMATH DE number 217454 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• New developments in the theory of Gröbner bases and applications to formal verification
• Parametric quantified SAT solving
• The Theory of Representation for Boolean Algebras
• Theory and Applications of Satisfiability Testing

Cited in

(9)

• 3BA: a border bases solver with a SAT extension
• On conversions from CNF to ANF
• On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers
• The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study
• Boolean Gröbner bases in SAT solving
• Boolean Rings for Intersection-Based Satisfiability
• BDD-guided clause generation
• A Gröbner Basis Approach to CNF-Formulae Preprocessing
• A greedy randomized adaptive search procedure (GRASP) for inferring logical clauses from examples in polynomial time and some extensions

Describes a project that uses

Uses Software

• MiniSat
• REDLOG

This page was built for publication: Extending Clause Learning of SAT Solvers with Boolean Gröbner Bases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3587716)