Quantifier reordering for QBF

DOI10.1007/S10817-015-9353-1MaRDI QIDQ287386zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Computing Resolution-Path Dependencies in Linear Time ,
• Integrating dependency schemes in search-based QBF solvers
• Dependency learning for QBF
• Variable independence and resolution paths for quantified Boolean formulas
• Dependency Learning for QBF

Cites work

• scientific article; zbMATH DE number 1470716 (Why is no real title available?)
• scientific article; zbMATH DE number 1798189 (Why is no real title available?)
• Backdoor sets of quantified Boolean formulas
• Blocked clause elimination for QBF
• Bounded-width QBF is PSPACE-complete
• Computing Resolution-Path Dependencies in Linear Time ,
• Integrating dependency schemes in search-based QBF solvers
• Resolution for quantified Boolean formulas
• The polynomial-time hierarchy
• Variable dependencies and Q-resolution
• Variable independence and resolution paths for quantified Boolean formulas

Cited in

(4)

• Dependency schemes for DQBF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Small resolution proofs for QBF using dependency treewidth
• Using decomposition-parameters for QBF: mind the prefix!

Describes a project that uses

Uses Software

• Bloqqer

This page was built for publication: Quantifier reordering for QBF

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