Abstraction-Based Algorithm for 2QBF

DOI10.1007/978-3-642-21581-0_19zbMath1330.68115OpenAlexW147950966MaRDI QIDQ3007686

Mikoláš Janota, João P. Marques-Silva

Publication date: 17 June 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-21581-0_19

Mathematics Subject Classification ID

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

Related Items

Quantified maximum satisfiability ⋮ QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving ⋮ Symmetry in Gardens of Eden ⋮ Synchronous counting and computational algorithm design ⋮ Never trust your solver: certification for SAT and QBF ⋮ Complexity-sensitive decision procedures for abstract argumentation ⋮ Computational complexity of flat and generic assumption-based argumentation, with and without probabilities ⋮ Refutation-based synthesis in SMT ⋮ Incremental Determinization ⋮ 2QBF: Challenges and Solutions ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ Expansion-based QBF solving versus Q-resolution ⋮ Backdoors to tractable answer set programming ⋮ Solving QBF with counterexample guided refinement

Uses Software

• MiniSat
• QuBE++
• sQueezeBF
• QBFLIB
• QUBE
• Mjollnir

Cites Work

• Solving satisfiability problems with preferences
• SAT-based planning in complex domains: Concurrency, constraints and nondeterminism
• Theory and applications of satisfiability testing -- SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
• A structure-preserving clause form translation
• A satisfiability procedure for quantified Boolean formulae
• Theory and applications of satisfiability testing. 6th international conference, SAT 2003, Santa Margherita Ligure, Italy, May 5--8, 2003. Selected revised papers
• The minimum equivalent DNF problem and shortest implicants
• Propositional circumscription and extended closed-world reasoning are \(\Pi_ 2^ P\)-complete
• Efficiently solving quantified bit-vector formulas
• Counterexample-guided abstraction refinement for symbolic model checking
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• The Seventh QBF Solvers Evaluation (QBFEVAL’10)
• Counterexample Guided Abstraction Refinement Algorithm for Propositional Circumscription
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Formal Methods in Computer-Aided Design
• Theory and Applications of Satisfiability Testing
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item