• Nenofex

  • Referenced in 18 articles [sw09579]
  • Nenofex: Expanding NNF for QBF Solving. The topic of this paper is Nenofex, a solver...
  • Bloqqer

  • Referenced in 30 articles [sw09578]
  • represented. However, the translation to processable QBF encodings is in general not unique ... variables and clauses not relevant for the solving process or blur information which could ... beneficial for the solving process. To deal with both of these issues, preprocessors have been ... introduced which rewrite a given QBF before it is passed to a solver. In this...
  • CirQit2

  • Referenced in 6 articles [sw11380]
  • Exploiting circuit representations in QBF solving. Previous work has shown that circuit representations...
  • 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 ... multicore boxes to clusters and grids, to solve more relevant instances and faster than previous ... state-of-the-art QBF Solver. It was able to solve more than twice...
  • HQSpre

  • Referenced in 10 articles [sw28634]
  • experiments show that HQSpre allows QBF solvers to solve more benchmark instances and is able...
  • MPIDepQBF

  • Referenced in 4 articles [sw18671]
  • MPIDepQBF: Towards parallel QBF solving without knowledge sharing. Inspired by recent work on parallel ... solving, we present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel ... uses a sequential state-of-the-art QBF solver to evaluate subformulas in working processes...
  • ToyElim

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

  • Referenced in 16 articles [sw06959]
  • point that some instances are solved directly by sQueezeBF -- and that it can significantly improve ... QBF solvers -- up to the point that some instances cannot be solved without sQueezeBF preprocessing...
  • Yasol

  • Referenced in 1 article [sw41488]
  • side as known from SAT- and QBF- solving, as well as with constraint learning...
  • Boolector

  • Referenced in 31 articles [sw00085]
  • Boolector: an efficient SMT solver for bit-vectors...
  • MiniSat

  • Referenced in 565 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • QuBE++

  • Referenced in 27 articles [sw00766]
  • In this paper we describe QuBE++, an efficient...
  • SMT-LIB

  • Referenced in 194 articles [sw04103]
  • SMT-LIB was created with the expectation that...
  • NuSMV

  • Referenced in 309 articles [sw04131]
  • NuSMV is a symbolic model checker developed as...
  • SATO

  • Referenced in 196 articles [sw04451]
  • SATO: A Solver for Propositional Satisfiability: The Davis...
  • SATIRE

  • Referenced in 39 articles [sw04648]
  • SATIRE: A new incremental satisfiability engine. We introduce...
  • cvc3

  • Referenced in 85 articles [sw04886]
  • CVC3 is an automatic theorem prover for Satisfiability...
  • z3

  • Referenced in 590 articles [sw04887]
  • Z3 is a high-performance theorem prover being...
  • WEKA

  • Referenced in 304 articles [sw06435]
  • WEKA: Waikato Environment for Knowledge Analysis. WEKA is...