Failed Literal Detection for QBF

DOI10.1007/978-3-642-21581-0_21zbMath1330.68118OpenAlexW178358665MaRDI QIDQ3007688

Florian Lonsing, Armin Biere

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_21

Mathematics Subject Classification ID

Related Items (5)

The QBF Gallery: behind the scenes ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Q-Resolution with Generalized Axioms ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ Solving QBF with counterexample guided refinement

Uses Software

• sQueezeBF
• PicoSAT
• Nenofex
• HeerHugo
• DepQBF
• Quantor

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theory and applications of satisfiability testing -- SAT 2010. 13th international conference, SAT 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Resolution for quantified Boolean formulas
• The propositional formula checker HeerHugo
• Theory and applications of satisfiability testing -- SAT 2007. 10th international conference, Lisbon, Portugal, May 28--31, 2007. Proceedings
• Nenofex: Expanding NNF for QBF Solving
• Using SAT in QBF
• A First Step Towards a Unified Proof Checker for QBF
• Bounded Universal Expansion for Preprocessing QBF
• Effective Incorporation of Double Look-Ahead Procedures
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• The Seventh QBF Solvers Evaluation (QBFEVAL’10)
• Variable Dependencies of Quantified CSPs
• Theory and Applications of Satisfiability Testing
• Binary Clause Reasoning in QBF

This page was built for publication: Failed Literal Detection for QBF