• Bloqqer

  • Referenced in 28 articles [sw09578]
  • Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... unique and may either introduce variables and clauses not relevant for the solving process ... preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied ... Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques...
  • Beaver

  • Referenced in 9 articles [sw00071]
  • Beaver: Engineering an efficient SMT solver for bit...
  • Boolector

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

  • Referenced in 611 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • MiniSat

  • Referenced in 536 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • R

  • Referenced in 8601 articles [sw00771]
  • R is a language and environment for statistical...
  • SCIP

  • Referenced in 472 articles [sw01091]
  • SCIP is currently one of the fastest non...
  • ML

  • Referenced in 517 articles [sw01218]
  • ML (’Meta Language’) is a general-purpose functional...
  • ALGOL 68

  • Referenced in 291 articles [sw01226]
  • ALGOL 68 (short for ALGOrithmic Language 1968) is...
  • UBCSAT

  • Referenced in 36 articles [sw02614]
  • UBCSAT: An implementation and experimentation environment for SLS...
  • VAMPIRE

  • Referenced in 239 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...
  • PVS

  • Referenced in 620 articles [sw03484]
  • PVS is a verification system: that is, a...
  • Eiffel

  • Referenced in 290 articles [sw03522]
  • Eiffel is an ISO-standardized, object-oriented programming...
  • CPLEX

  • Referenced in 2583 articles [sw04082]
  • IBM® ILOG® CPLEX® offers C, C++, Java, .NET...
  • SPASS

  • Referenced in 178 articles [sw04108]
  • SPASS is an automated theorem prover for first...
  • TPTP

  • Referenced in 378 articles [sw04143]
  • The TPTP (Thousands of Problems for Theorem Provers...
  • CUDD

  • Referenced in 148 articles [sw04446]
  • The CUDD package provides functions to manipulate Binary...
  • SATO

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

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