Blocked Clause Elimination for QBF

DOI10.1007/978-3-642-22438-6_10zbMath1341.68181OpenAlexW99602494MaRDI QIDQ5200018

Martina Seidl, Armin Biere, Florian Lonsing

Publication date: 29 July 2011

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-22438-6_10

Mathematics Subject Classification ID

Classical propositional logic (03B05)

Related Items

Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving, Solution validation and extraction for QBF preprocessing, The QBF Gallery: behind the scenes, Quantifier reordering for QBF, Preprocessing for DQBF, Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API, QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving, Simulating circuit-level simplifications on CNF, Conformant planning as a case study of incremental QBF solving, Symmetry in Gardens of Eden, Long-distance Q-resolution with dependency schemes, BOCoSy: Small but Powerful Symbolic Output-Feedback Control, Algorithms for computing minimal equivalent subformulas, Truth Assignments as Conditional Autarkies, Encodings of Bounded Synthesis, Incremental Determinization, Q-Resolution with Generalized Axioms, 2QBF: Challenges and Solutions, Long Distance Q-Resolution with Dependency Schemes, Dual proof generation for quantified Boolean formulas with a BDD-based solver, Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations, Bloqqer, The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17), The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, CAQE and QuAbS: Abstraction Based QBF Solvers, Planning with Incomplete Information in Quantified Answer Set Programming, Solving QBF with counterexample guided refinement, SAT-Inspired Eliminations for Superposition

Uses Software

• MiniSat
• sQueezeBF
• Nenofex
• DepQBF
• QUBE
• Quantor

Cites Work

• Unnamed Item
• A structure-preserving clause form translation
• Resolution for quantified Boolean formulas
• On a generalization of extended resolution
• Nenofex: Expanding NNF for QBF Solving
• Blocked Clause Elimination
• Bounded Universal Expansion for Preprocessing QBF
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• Clause Elimination Procedures for CNF Formulas
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing