• Nenofex

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

  • Referenced in 27 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...
  • 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 14 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...
  • HQSpre

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

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

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

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

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

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

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

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

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

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

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

  • Referenced in 567 articles [sw06916]
  • Chaff:engineering an efficient SAT solver. Boolean Satisfiability...