Integrating Dependency Schemes in Search-Based QBF Solvers

DOI10.1007/978-3-642-14186-7_14zbMath1306.68165OpenAlexW1603914046MaRDI QIDQ4930586

Armin Biere, Florian Lonsing

Publication date: 29 September 2010

Published in: Theory and Applications of Satisfiability Testing – SAT 2010 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-14186-7_14

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (14)

Backdoors to Normality for Disjunctive Logic Programs ⋮ Quantifier reordering for QBF ⋮ Small Resolution Proofs for QBF using Dependency Treewidth ⋮ Symmetry in Gardens of Eden ⋮ Long-distance Q-resolution with dependency schemes ⋮ Logic-based ontology comparison and module extraction, with an application to DL-Lite ⋮ Soundness of \(\mathcal{Q}\)-resolution with dependency schemes ⋮ Never trust your solver: certification for SAT and QBF ⋮ Towards Uniform Certification in QBF ⋮ Efficiently solving quantified bit-vector formulas ⋮ Dependency Schemes for DQBF ⋮ HordeQBF: A Modular and Massively Parallel QBF Solver ⋮ Using decomposition-parameters for QBF: mind the prefix! ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers

Uses Software

• Chaff
• Quaffle
• DepQBF

This page was built for publication: Integrating Dependency Schemes in Search-Based QBF Solvers