Toward leaner binary-clause reasoning in a satisfiability solver

DOI10.1007/S10472-005-0433-5MaRDI QIDQ1777406zbMATH OpenOpenAlexFDO

Authors Allen Van Gelder

Publication date 13 May 2005

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-005-0433-5

Mathematics Subject Classification ID

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

Recommendations

• Combining preorder and postorder resolution in a satisfiability solver
• BerkMin: A fast and robust SAT-solver
• Binary Clause Reasoning in QBF
• Simplifying binary propositional theories into connected components twice as fast
• scientific article; zbMATH DE number 2243370

Cites work

• scientific article; zbMATH DE number 956865 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A machine program for theorem-proving
• A strong-connectivity algorithm and its applications in data flow analysis
• An efficient algorithm for the 3-satisfiability problem
• Eliminating dublication with the hyper-linking strategy
• Introduction to algorithms
• SATO: An efficient propositional prover

Cited in

(10)

• Producing and verifying extremely large propositional refutations
• On preprocessing techniques and their impact on propositional model counting
• Binary Clause Reasoning in QBF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Simplifying binary propositional theories into connected components twice as fast
• Efficient CNF simplification based on binary implication graphs
• SAT encodings for pseudo-Boolean constraints together with at-most-one constraints
• Simulating circuit-level simplifications on CNF
• Preprocessing for DQBF
• The configurable SAT solver challenge (CSSC)

Describes a project that uses

Uses Software

• DIMACS
• Chaff
• SATO

This page was built for publication: Toward leaner binary-clause reasoning in a satisfiability solver

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