Quantifier reordering for QBF

DOI10.1007/s10817-015-9353-1zbMath1356.68200OpenAlexW2262500273MaRDI QIDQ287386

Friedrich Slivovsky, Stefan Szeider

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-015-9353-1

zbMATH Keywords

Q-resolutionquantified Boolean formulasquantifier reorderingvariable dependencies

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (4)

Small Resolution Proofs for QBF using Dependency Treewidth ⋮ Dependency Schemes for DQBF ⋮ Using decomposition-parameters for QBF: mind the prefix! ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1

Uses Software

• Bloqqer

Cites Work

• Unnamed Item
• Unnamed Item
• Backdoor sets of quantified Boolean formulas
• The polynomial-time hierarchy
• Resolution for quantified Boolean formulas
• Computing Resolution-Path Dependencies in Linear Time ,
• Bounded-width QBF is PSPACE-complete
• Variable Independence and Resolution Paths for Quantified Boolean Formulas
• Variable Dependencies and Q-Resolution
• Integrating Dependency Schemes in Search-Based QBF Solvers
• Blocked Clause Elimination for QBF

This page was built for publication: Quantifier reordering for QBF