Bounded Universal Expansion for Preprocessing QBF
From MaRDI portal
Publication:3612470
DOI10.1007/978-3-540-72788-0_24zbMath1214.68331OpenAlexW1494899888MaRDI QIDQ3612470
Hans Kleine Büning, Uwe Bubeck
Publication date: 10 March 2009
Published in: Theory and Applications of Satisfiability Testing – SAT 2007 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-72788-0_24
Related Items (13)
Solution validation and extraction for QBF preprocessing ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Models and quantifier elimination for quantified Horn formulas ⋮ Failed Literal Detection for QBF ⋮ Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers ⋮ Blocked Clause Elimination for QBF ⋮ Dependency Schemes for DQBF ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ A Compact Representation for Syntactic Dependencies in QBFs ⋮ Backdoor sets of quantified Boolean formulas ⋮ Expansion-based QBF solving versus Q-resolution ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Solving QBF with counterexample guided refinement
Uses Software
This page was built for publication: Bounded Universal Expansion for Preprocessing QBF
