Variable independence and resolution paths for quantified Boolean formulas

DOI10.1007/978-3-642-23786-7_59MaRDI QIDQ3169452zbMATH OpenOpenAlexFDO

Authors Allen Van Gelder

Publication date 23 September 2011

Published in Principles and Practice of Constraint Programming – CP 2011 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-23786-7_59

Mathematics Subject Classification ID

Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Variable dependencies and Q-resolution
• Computing Resolution-Path Dependencies in Linear Time ,
• Dependency learning for QBF
• Dependency Learning for QBF
• Dependency schemes for DQBF

Cited in

(15)

• Dependency learning for QBF
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Solution validation and extraction for QBF preprocessing
• Long-distance Q-resolution with dependency schemes
• Dependency schemes for DQBF
• Long distance Q-resolution with dependency schemes
• Quantifier reordering for QBF
• Variable dependencies and Q-resolution
• Small resolution proofs for QBF using dependency treewidth
• Preprocessing for DQBF
• Exploiting resolution-based representations for MaxSAT solving
• A Compact Representation for Syntactic Dependencies in QBFs
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Variable Dependencies of Quantified CSPs
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes

This page was built for publication: Variable independence and resolution paths for quantified Boolean formulas

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