Dependency learning for QBF

DOI10.1007/978-3-319-66263-3_19MaRDI QIDQ1680261zbMATH OpenOpenAlexFDO

Authors Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider

Publication date 15 November 2017

Full work available at URL http://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3440

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
• Integrating dependency schemes in search-based QBF solvers
• Variable dependencies and Q-resolution
• Variable independence and resolution paths for quantified Boolean formulas
• Dependency schemes for DQBF

Cited in

(31)

• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Integrating dependency schemes in search-based QBF solvers
• Dependency schemes for DQBF
• Dependency Learning for QBF
• Variable independence and resolution paths for quantified Boolean formulas
• Quantifier reordering for QBF
• Knowledge representation analysis of graph mining
• Combining resolution-path dependencies with dependency learning
• Dynamic QBF dependencies in reduction and expansion
• Building strategies into QBF proofs
• Incremental QBF solving by DepQBF
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• scientific article; zbMATH DE number 7447736 (Why is no real title available?)
• Variable dependencies and Q-resolution
• A Compact Representation for Syntactic Dependencies in QBFs
• From DQBF to QBF by dependency elimination
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• Moving definition variables in quantified Boolean formulas
• Long-distance Q-resolution with dependency schemes
• Clausal abstraction for DQBF
• ALLQBF solving by computational learning
• scientific article; zbMATH DE number 7533347 (Why is no real title available?)
• Learning to integrate deduction and search in reasoning about quantified Boolean formulas
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Learning an extension of the class of functional dependencies with queries
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• scientific article; zbMATH DE number 7559123 (Why is no real title available?)
• Solving dependency quantified Boolean formulas using quantifier localization

Describes a project that uses

Uses Software

• Nenofex
• CAQE
• AIGSolve

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