Variable dependencies and Q-resolution

DOI10.1007/978-3-319-09284-3_21MaRDI QIDQ3192076zbMATH OpenOpenAlexFDO

Authors Friedrich Slivovsky, Stefan Szeider

Publication date 26 September 2014

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

Full work available at URL https://doi.org/10.1007/978-3-319-09284-3_21

Mathematics Subject Classification ID

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

Recommendations

• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Variable independence and resolution paths for quantified Boolean formulas
• Dependency learning for QBF
• Computing Resolution-Path Dependencies in Linear Time ,
• Long-distance Q-resolution with dependency schemes

Cited in

(17)

• Dependency learning for QBF
• A resolution-style proof system for DQBF
• Combining resolution-path dependencies with dependency learning
• Using decomposition-parameters for QBF: mind the prefix!
• Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
• Long-distance Q-resolution with dependency schemes
• On Stronger Calculi for QBFs
• Q-resolution with generalized axioms
• Lifting QBF resolution calculi to DQBF
• Long distance Q-resolution with dependency schemes
• Quantifier reordering for QBF
• Quasi-dependent variables in hybrid automata
• Variable independence and resolution paths for quantified Boolean formulas
• Small resolution proofs for QBF using dependency treewidth
• Integrating dependency schemes in search-based QBF solvers
• Dynamic QBF dependencies in reduction and expansion
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes

This page was built for publication: Variable dependencies and Q-resolution

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