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)

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

Describes a project that uses

Uses Software

• AIGSolve
• CAQE
• Nenofex

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)