An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
From MaRDI portal
Publication:1610666
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
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items
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
