A solver for QBFs in negation normal form

DOI10.1007/s10601-008-9055-yzbMath1167.68054OpenAlexW2161955489MaRDI QIDQ1020501

Stefan Woltran, Uwe Egly, Martina Seidl

Publication date: 29 May 2009

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-008-9055-y

zbMATH Keywords

solvernegation normal formQBFs

Mathematics Subject Classification ID

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

Related Items (10)

A first polynomial non-clausal class in many-valued logic ⋮ Unnamed Item ⋮ Efficiently solving quantified bit-vector formulas ⋮ A complexity perspective on entailment of parameterized linear constraints ⋮ Non-prenex QBF Solving Using Abstraction ⋮ On Stronger Calculi for QBFs ⋮ Beyond CNF: A Circuit-Based QBF Solver ⋮ Encoding deductive argumentation in quantified Boolean formulae ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ The possibilistic Horn non-clausal knowledge bases

Uses Software

• Quaffle
• QUBOS
• Quantor
• semprop
• KoMeT
• sKizzo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On different structure-preserving translations to normal form
• The complexity of nested counterfactuals and iterated knowledge base revisions
• Backjumping for quantified Boolean logic satisfiability
• A structure-preserving clause form translation
• An optimality result for clause form translation
• Logic programming and knowledge representation---The A-Prolog perspective
• Reducing Preferential Paraconsistent Reasoning to Classical Entailment
• Theory and Applications of Satisfiability Testing
• Automated Deduction – CADE-20
• Logic Programming and Nonmonotonic Reasoning
• Inconsistency Tolerance
• Logic Programming
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
• Binary Clause Reasoning in QBF
• Automated Deduction – CADE-19
• Counterfactuals

This page was built for publication: A solver for QBFs in negation normal form