Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits

DOI10.1007/978-3-642-02777-2_36zbMath1247.68237OpenAlexW1605407652MaRDI QIDQ3637174

Hans Kleine Büning, Zhao, Xishun, Uwe Bubeck

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02777-2_36

Mathematics Subject Classification ID

Related Items (7)

Quantified maximum satisfiability ⋮ Quantified Constraints in Twenty Seventeen ⋮ The Complexity Landscape of Outcome Determination in Judgment Aggregation ⋮ Anti-alignments in Conformance Checking – The Dark Side of Process Models ⋮ How QBF expansion makes strategy extraction hard ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ Hardness and optimality in QBF proof systems modulo NP

Uses Software

• Nenofex

Cites Work

• Unnamed Item
• Models and quantifier elimination for quantified Horn formulas
• The equivalence of Horn and network complexity for Boolean functions
• Resolution for quantified Boolean formulas
• Nenofex: Expanding NNF for QBF Solving
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

This page was built for publication: Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits