Learning to integrate deduction and search in reasoning about quantified Boolean formulas

DOI10.1007/978-3-642-04222-5_22MaRDI QIDQ3655211zbMATH OpenOpenAlexFDO

Authors Luca Pulina, Armando Tacchella

Publication date 7 January 2010

Published in Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-04222-5_22

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)

Recommendations

• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Dependency Learning for QBF
• Dependency learning for QBF
• ALLQBF solving by computational learning
• QELL: QBF reasoning with extended clause learning and levelized SAT solving

Cites work

• A comparison of structural CSP decomposition methods
• A linear time algorithm for finding tree-decompositions of small treewidth
• A self-adaptive multi-engine solver for quantified Boolean formulas
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Automated Deduction – CADE-20
• Backjumping for quantified Boolean logic satisfiability
• Binary Clause Reasoning in QBF
• Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• Computer Science Logic
• scientific article; zbMATH DE number 823069 (Why is no real title available?)
• scientific article; zbMATH DE number 2200689 (Why is no real title available?)
• Principles and Practice of Constraint Programming – CP 2004
• Resolution for quantified Boolean formulas
• Resolution versus search: Two strategies for SAT
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings

Cited in

(2)

• Validating QBF Validity in HOL4
• Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation

Describes a project that uses

Uses Software

• LIBSVM
• C4.5
• sKizzo
• Quantor

This page was built for publication: Learning to integrate deduction and search in reasoning about quantified Boolean formulas

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