Binary Clause Reasoning in QBF

DOI10.1007/11814948_33zbMATH Open1187.68265OpenAlexW1581900214MaRDI QIDQ5756571FDOQ5756571

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

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

Mathematics Subject Classification ID

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

Cited In (9)

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

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)