Dependency Learning for QBF

DOI10.1613/JAIR.1.11529MaRDI QIDQ4968372zbMATH OpenOpenAlexWikidataFDO

Authors Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider

Publication date 12 July 2019

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1613/jair.1.11529

zbMATH Keywords

quantified Boolean formulas (QBFs)quantified conflict-driven clause learning

Mathematics Subject Classification ID

Complexity of proofs (03F20) Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Dependency learning for QBF
• Learning an extension of the class of functional dependencies with queries
• Integrating dependency schemes in search-based QBF solvers
• From DQBF to QBF by dependency elimination
• A Compact Representation for Syntactic Dependencies in QBFs
• Incremental QBF solving by DepQBF
• Exact learning of multivalued dependency formulas
• On learning multivalued dependencies with queries
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Solving dependency quantified Boolean formulas using quantifier localization

Cited in

(32)

• Dependency learning for QBF
• From DQBF to QBF by dependency elimination
• Lower bounds for QCDCL via formula gauge
• Proof complexity of symbolic QBF reasoning
• Solving dependency quantified Boolean formulas using quantifier localization
• Combining resolution-path dependencies with dependency learning
• Learning an extension of the class of functional dependencies with queries
• Dependency schemes for DQBF
• Quantifier reordering for QBF
• Incremental QBF solving by DepQBF
• Variable independence and resolution paths for quantified Boolean formulas
• A Compact Representation for Syntactic Dependencies in QBFs
• Learning to integrate deduction and search in reasoning about quantified Boolean formulas
• ALLQBF solving by computational learning
• Integrating dependency schemes in search-based QBF solvers
• Dynamic QBF dependencies in reduction and expansion
• Planning with Incomplete Information in Quantified Answer Set Programming
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Theory and Applications of Satisfiability Testing
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• Lower bounds for QCDCL via formula gauge
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• Towards Uniform Certification in QBF
• Should Decisions in QCDCL Follow Prefix Order?
• Moving definition variables in quantified Boolean formulas
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
• Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
• Strong (D)QBF dependency schemes via implication-free resolution paths
• QCDCL with cube learning or pure literal elimination -- what is best?
• Quantifier shifting for quantified Boolean formulas revisited
• Understanding the relative strength of QBF CDCL solvers and QBF resolution

This page was built for publication: Dependency Learning for QBF

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