A solver for QBFs in negation normal form

DOI10.1007/S10601-008-9055-YzbMATH Open1167.68054OpenAlexW2161955489MaRDI QIDQ1020501FDOQ1020501

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

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

zbMATH Keywords

solvernegation normal formQBFs

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (10)

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

Uses Software

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

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)