An algorithm to evaluate quantified Boolean formulae and its experimental evaluation

DOI10.1023/A:1015019416843zbMath1002.68165OpenAlexW1862403209MaRDI QIDQ1610666

Andrea Giovanardi, Marco Cadoli, Massimo Giovanardi, Marco Schaerf

Publication date: 20 August 2002

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1015019416843

zbMATH Keywords

quantified Boolean formulae

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (25)

The complexity of constraint satisfaction games and QCSP ⋮ Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ⋮ Solving quantified constraint satisfaction problems ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Long-distance Q-resolution with dependency schemes ⋮ Soundness of \(\mathcal{Q}\)-resolution with dependency schemes ⋮ Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable ⋮ Henkin quantifiers and Boolean formulae: a certification perspective of DQBF ⋮ Unified QBF certification and its applications ⋮ Compiling problem specifications into SAT ⋮ Failed Literal Detection for QBF ⋮ Computational methods for database repair by signed formulae ⋮ A Unified Framework for Certificate and Compilation for QBF ⋮ Incremental Determinization ⋮ On Q-Resolution and CDCL QBF Solving ⋮ Long Distance Q-Resolution with Dependency Schemes ⋮ Value ordering for quantified CSPs ⋮ Non-binary quantified CSP: Algorithms and modelling ⋮ Expansion-based QBF solving versus Q-resolution ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Backjumping for quantified Boolean logic satisfiability ⋮ Complexity results for explanations in the structural-model approach

This page was built for publication: An algorithm to evaluate quantified Boolean formulae and its experimental evaluation