Binary Clause Reasoning in QBF

DOI10.1007/11814948_33zbMATH Open1187.68265OpenAlexW1581900214MaRDI QIDQ5756571FDOQ5756571

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)

Cited In (8)

• 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
• Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas
• Backdoor sets of quantified Boolean formulas
• Failed Literal Detection for QBF
• Theory and Applications of Satisfiability Testing
• A solver for QBFs in negation normal form

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)