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

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

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

(26)

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

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)