• Quaffle

  • Referenced in 64 articles [sw07278]
  • Evaluator with Learning Quaffle is an experimental QBF solver. The idea of this solver ... with two other state of the art QBF solvers QuBE and Semprop is available here...
  • Bloqqer

  • Referenced in 28 articles [sw09578]
  • Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... various application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques ... represented. However, the translation to processable QBF encodings is in general not unique ... have been introduced which rewrite a given QBF before it is passed to a solver...
  • DepQBF

  • Referenced in 31 articles [sw09734]
  • search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form ... based on the DPLL algorithm for QBF with conflict-driven clause and solution-driven cube...
  • Quantor

  • Referenced in 22 articles [sw28381]
  • work correctly in the context of QBF. Both features are described in our paper ”Effective ... solver for quantified boolean formulas (QBF) in the QDIMACS format. Checking satisfiability ... QBF, the QBF problem, is the standard PSPACE complete problem. Many practically important problems, such ... model checking can be formulated succinctly in QBF. In our recent talk...
  • QUBE

  • Referenced in 29 articles [sw11381]
  • satisfiability of a Quantified Boolean Formula (QBF) is an important research issue in Artificial Intelligence ... problem of deciding the satisfiability of a QBF. In this paper we present QuBE...
  • QuBE++

  • Referenced in 28 articles [sw00766]
  • knowledge, QuBE++ is the first QBF reasoning engine that uses lazy data structures both ... those of other state-of-the-art QBF engines, and are comparable with the best...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • Nenofex: Expanding NNF for QBF Solving. The topic of this paper is Nenofex, a solver ... quantified boolean formulae (QBF) in negation normal form (NNF), which relies on expansion ... limit less frequently than a resolution-based QBF solver for CNF, but also that there...
  • QBFLIB

  • Referenced in 17 articles [sw09581]
  • tools related to Quantified Boolean Formula (QBF) satisfiability. QBFLIB is meant as a service ... QBF research community and its main goal is to provide an uniform test ... empirical characterization of QBF solvers...
  • sQueezeBF

  • Referenced in 15 articles [sw06959]
  • range of state-of-the-art QBF solvers -- up to the point that some instances...
  • CAQE

  • Referenced in 9 articles [sw25922]
  • CAQE: a certifying QBF solver. We present a new CEGAR-based algorithm ... QBF. The algorithm builds on a decomposition of QBFs into a sequence of propositional formulas ... CAQE has competitive performance compared to current QBF solvers and outperforms previous certifying solvers...
  • CirQit2

  • Referenced in 6 articles [sw11380]
  • Exploiting circuit representations in QBF solving. Previous work has shown that circuit representations ... exploited in QBF solvers to obtain useful performance improvements. In this paper we examine some ... have implemented these techniques in a new QBF solver called CirQit2 and evaluated their impact...
  • PaQuBE

  • Referenced in 5 articles [sw06998]
  • PaQuBE: Distributed QBF solving with advanced knowledge sharing. n this paper we present the parallel ... QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited ... shared. According to the last QBF Evaluation, QuBE is the most powerful state ... QBF Solver. It was able to solve more than twice as many benchmarks...
  • QBFEVAL

  • Referenced in 4 articles [sw22901]
  • QBF Solver Evaluation Portal. QBF Evaluations are a series of yearly events with the purpose ... field of QBF solvers and QBF-based applications. Up to the third event ... competitive event. We warmly encourage developers of QBF solvers to submit their work, even ... requirements. We also welcome the submission of QBF formulas to be used as test instances...
  • QMiraXT

  • Referenced in 4 articles [sw11456]
  • QMiraXT - A multithreaded QBF solver. Dieser DPLL such-basierte Solver ist eine Erweiterung des multi ... MiraXT. QMiraXT ist der erste moderne parallele QBF Solver, der knowledge sharing unterstützt ... viele Beschleunigungstechniken moderner SAT Solver in die QBF Domäne eingeführt. Dieses Tool unterstützt fortgeschrittene Techniken ... Single Quantification Level Scheduling Algorithmus für parallele QBF Solver, welcher es erlaubt, große QBF Probleme...
  • MPIDepQBF

  • Referenced in 4 articles [sw18671]
  • MPIDepQBF: Towards parallel QBF solving without knowledge sharing. Inspired by recent work on parallel ... uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes ... equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated...
  • Squolem

  • Referenced in 3 articles [sw09453]
  • Validating QBF invalidity in HOL4. The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates ... benefit from Squolem’s automation for QBF problems, and provides high correctness assurances for Squolem ... certificate checking is feasible even for large QBF instances. Our work prompted improvements to HOL4...
  • ToyElim

  • Referenced in 3 articles [sw09900]
  • interpolants, certain forms of abduction, SAT and QBF solving, and processing of formulas according ... applications. It however transparently passes identified SAT, QBF and variable elimination subproblems to efficient external...
  • HordeQBF

  • Referenced in 2 articles [sw18670]
  • Hordeqbf: A modular and massively parallel QBF solver. The recently developed massively parallel satisfiability ... integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain ... massively parallel QBF solver--HordeQBF. In this paper we describe the details of this integration ... hard application instances of the 2014 QBF Gallery...
  • AIGSolve

  • Referenced in 2 articles [sw25923]
  • QBF solver AIGSolve. AIGSolve is a rewriting-based solver based on And-Inverter Graphs (AIGs ... compaction of the representations, methods for preprocessing QBF-formulas based on incremental SAT, heuristics that...
  • HQSpre

  • Referenced in 2 articles [sw28634]
  • HQSpre - An Effective Preprocessor for QBF and DQBF. We present our new preprocessor HQSpre ... used. Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances...