A solver for QBFs in negation normal form

DOI10.1007/S10601-008-9055-YMaRDI QIDQ1020501zbMATH OpenOpenAlexFDO

Authors Uwe Egly, Martina Seidl, Stefan Woltran

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

negation normal formQBFssolver

Mathematics Subject Classification ID

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

Recommendations

• A non-prenex, non-clausal QBF solver with game-state learning
• Beyond CNF: A Circuit-Based QBF Solver
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2004

Cites work

• A structure-preserving clause form translation
• An optimality result for clause form translation
• Automated Deduction – CADE-20
• Backjumping for quantified Boolean logic satisfiability
• Binary Clause Reasoning in QBF
• Counterfactuals
• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 1303351 (Why is no real title available?)
• scientific article; zbMATH DE number 1305704 (Why is no real title available?)
• scientific article; zbMATH DE number 1342207 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1950260 (Why is no real title available?)
• scientific article; zbMATH DE number 1979551 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 3074068 (Why is no real title available?)
• Inconsistency Tolerance
• Logic Programming
• Logic programming and knowledge representation---The A-Prolog perspective
• Logic Programming and Nonmonotonic Reasoning
• On different structure-preserving translations to normal form
• Optimizing a BDD-based modal solver.
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
• Reducing Preferential Paraconsistent Reasoning to Classical Entailment
• Report of the third QBF solvers evaluation
• The complexity of nested counterfactuals and iterated knowledge base revisions
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing

Cited in

(10)

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

Describes a project that uses

Uses Software

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

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

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