Binary Clause Reasoning in QBF

DOI10.1007/11814948_33MaRDI QIDQ5756571zbMATHOpenAlexFDO

Authors Horst Samulowitz, Fahiem Bacchus

Publication date 4 September 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814948_33

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• QELL: QBF reasoning with extended clause learning and levelized SAT solving
• Toward leaner binary-clause reasoning in a satisfiability solver
• Contributions to the theory of practical quantified Boolean formula solving
• Theory and Applications of Satisfiability Testing
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas

Cited in

(9)

• Logic-based ontology comparison and module extraction, with an application to DL-Lite
• A solver for QBFs in negation normal form
• Backdoor sets of quantified Boolean formulas
• Theory and Applications of Satisfiability Testing
• Solving QBF with counterexample guided refinement
• Failed literal detection for QBF
• Learning to integrate deduction and search in reasoning about quantified Boolean formulas
• Toward leaner binary-clause reasoning in a satisfiability solver
• Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation

This page was built for publication: Binary Clause Reasoning in QBF

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