• Quaffle

  • Referenced in 66 articles [sw07278]
  • with Learning Quaffle is an experimental QBF solver. The idea of this solver is described ... Driven Learning in a Quantified Boolean Satisfiability Solver”, Proceedings of International Conference on Computer Aided ... other state of the art QBF solvers QuBE and Semprop is available here. The benchmarks...
  • Bloqqer

  • Referenced in 30 articles [sw09578]
  • application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques ... performance of such a solver usually depends on the way a problem is represented. However ... translation to processable QBF encodings is in general not unique and may either introduce variables ... rewrite a given QBF before it is passed to a solver. In this paper...
  • CAQE

  • Referenced in 16 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 ... false, QBFs; allowing us to certify the solver result. We implemented the algorithm ... competitive performance compared to current QBF solvers and outperforms previous certifying solvers...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form ... less frequently than a resolution-based QBF solver for CNF, but also that there...
  • QBFLIB

  • Referenced in 16 articles [sw09581]
  • collection of instances, solvers, and tools related to Quantified Boolean Formula (QBF) satisfiability. QBFLIB ... empirical characterization of QBF solvers...
  • sQueezeBF

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

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

  • Referenced in 10 articles [sw28634]
  • HQSpre - An Effective Preprocessor for QBF and DQBF. We present our new preprocessor HQSpre ... possible to tailor it towards different solver back-ends, e. g., to preserve the circuit ... Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances...
  • CirQit2

  • Referenced in 6 articles [sw11380]
  • circuit representations can be exploited in QBF solvers to obtain useful performance improvements. In this ... implemented these techniques in a new QBF solver called CirQit2 and evaluated their impact experimentally...
  • Quantor

  • Referenced in 22 articles [sw28381]
  • work correctly in the context of QBF. Both features are described in our paper ”Effective ... SATeLite. Quantor is a solver for quantified boolean formulas (QBF) in the QDIMACS format. Checking ... mention 7 applications. More information on the QBF problem can be found at QBFLIB ... submitted to the SAT’04 SAT Solver Competition. This application is described in more detail...
  • 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 ... event. We warmly encourage developers of QBF solvers to submit their work, even at early ... requirements. We also welcome the submission of QBF formulas to be used as test instances...
  • PaQuBE

  • Referenced in 5 articles [sw06998]
  • this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional ... relevant instances and faster than previous generation solvers. PaQuBE extends QuBE, its sequential core ... shared. According to the last QBF Evaluation, QuBE ... most powerful state-of-the-art QBF Solver. It was able to solve more than...
  • QMiraXT

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

  • Referenced in 27 articles [sw00766]
  • this paper we describe QuBE++, an efficient solver for Quantified Boolean Formulas (QBFs ... knowledge, QuBE++ is the first QBF reasoning engine that uses lazy data structures both ... robust solver, whose performances exceed those of other state-of-the-art QBF engines...
  • MPIDepQBF

  • Referenced in 4 articles [sw18671]
  • sequential state-of-the-art QBF solver to evaluate subformulas in working processes. It abstains ... equipped the state-of-the-art QBF solver DepQBF with assumption-based reasoning and integrated...
  • HordeQBF

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

  • Referenced in 3 articles [sw09453]
  • HOL4. The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates of invalidity, based ... benefit from Squolem’s automation for QBF problems, and provides high correctness assurances for Squolem...
  • 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...
  • QBFFam

  • Referenced in 1 article [sw41579]
  • systems underlie the reasoning power of QBF solvers. With our tool, it is possible...
  • Yasol

  • Referenced in 1 article [sw41488]
  • that there are no other Q-MIP solver at this time - Jan. 2017, most basic ... typically performed in SAT- and QBF- solvers, we have extended the Alphabeta-algorithm as roughly ... primal side as known from SAT- and QBF- solving, as well as with constraint learning...