Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas

DOI10.1007/978-3-642-04222-5_22zbMath1193.68214OpenAlexW1566051759MaRDI QIDQ3655211

Armando Tacchella, Luca Pulina

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)

Related Items

Validating QBF Validity in HOL4

Uses Software

• LIBSVM
• C4.5
• Quantor
• sKizzo

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Backjumping for quantified Boolean logic satisfiability
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Boosting search with variable elimination in constraint optimization and constraint satisfaction problems
• A comparison of structural CSP decomposition methods
• Resolution for quantified Boolean formulas
• Resolution versus search: Two strategies for SAT
• A linear time algorithm for finding tree-decompositions of small treewidth
• Theory and Applications of Satisfiability Testing
• Computer Science Logic
• Automated Deduction – CADE-20
• Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings
• Theory and Applications of Satisfiability Testing
• Binary Clause Reasoning in QBF
• Principles and Practice of Constraint Programming – CP 2004