• Quaffle

  • Referenced in 64 articles [sw07278]
  • Quaffle: Quantified Boolean Formula Evaluator with Learning Quaffle is an experimental QBF solver. The idea ... Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver”, Proceedings of 8th International Conference...
  • QUBE

  • Referenced in 28 articles [sw11381]
  • QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability. Deciding the satisfiability of a Quantified...
  • DepQBF

  • Referenced in 31 articles [sw09734]
  • search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form...
  • Bloqqer

  • Referenced in 28 articles [sw09578]
  • Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural...
  • QuBE++

  • Referenced in 27 articles [sw00766]
  • describe QuBE++, an efficient solver for Quantified Boolean Formulas (QBFs). To the extent...
  • semprop

  • Referenced in 17 articles [sw28383]
  • model caching in decision procedures for quantified Boolean formulas. The increasing role of quantified Boolean ... selection in semantic tree procedures for quantified Boolean formulas, learning methods are more important than...
  • QBFLIB

  • Referenced in 16 articles [sw09581]
  • Quantified Boolean formulas satisfiability library (QBFLIB). QBFLIB is a collection of instances, solvers, and tools ... related to Quantified Boolean Formula (QBF) satisfiability. QBFLIB is meant as a service...
  • Quantor

  • Referenced in 22 articles [sw28381]
  • SATeLite. Quantor is a solver for quantified boolean formulas (QBF) in the QDIMACS format. Checking...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form ... eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes...
  • MPIDepQBF

  • Referenced in 4 articles [sw18671]
  • present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular...
  • QUBOS

  • Referenced in 24 articles [sw09580]
  • quantified Boolean logic. The procedure is based on nonclausal simplification techniques that reduce formulae...
  • HQSpre

  • Referenced in 2 articles [sw28634]
  • tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified ... Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding so-called ... Henkin-quantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed...
  • Squolem

  • Referenced in 3 articles [sw09453]
  • Validating QBF invalidity in HOL4. The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates...
  • HordeQBF

  • Referenced in 2 articles [sw18670]
  • core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT...
  • ToyElim

  • Referenced in 3 articles [sw09900]
  • equivalent formula without these operators. Tasks like elimination of Boolean quantifiers, computation of uniform interpolants ... solving, and processing of formulas according to various semantics of logic programming can be expressed...
  • SMCHR

  • Referenced in 2 articles [sw09322]
  • with a modern Boolean satisfiability (SAT) solver for quantifier-free formulae with an arbitrary propositional...
  • Beaver

  • Referenced in 9 articles [sw00071]
  • solver (theorem prover) for the theory of quantifier-free finite-precision bit-vector arithmetic ... Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich ... nonlinear arithmetic) and equivalence checking (rich Boolean structure...
  • DDDLIB

  • Referenced in 1 article [sw00192]
  • constructing formulae with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding...
  • STABLE

  • Referenced in 2 articles [sw11913]
  • Boolean reasoning with computer algebra. This paper presents a new SMT solver, STABLE, for formulas ... quantifier-free logic over fixed-sized bit vectors (QF-BV). The heart of STABLE...
  • SONOLAR

  • Referenced in 2 articles [sw26291]
  • Solver that solves quantifier-free fixed-size bit-vector logic formulas. The solver supports ... blasting to translate bitvector constraints to a Boolean formula and lets a SAT solver decide...