• z3

  • Referenced in 603 articles [sw04887]
  • vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program...
  • QEPCAD

  • Referenced in 283 articles [sw00752]
  • using CADs. QEPCAD is an implementation of quantifier elimination by partial cylindrical algebraic decomposition...
  • plfit

  • Referenced in 269 articles [sw23186]
  • principled statistical framework for discerning and quantifying power-law behavior in empirical data. Our approach...
  • Yices

  • Referenced in 156 articles [sw04436]
  • records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT...
  • MONA

  • Referenced in 134 articles [sw06170]
  • data structures. We describe these techniques and quantify their respective effects by experimenting with separate...
  • Quaffle

  • Referenced in 68 articles [sw07278]
  • Quaffle: Quantified Boolean Formula Evaluator with Learning Quaffle is an experimental QBF solver. The idea ... Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver”, Proceedings of 8th International ... Malik, ”Conflict Driven Learning in a Quantified Boolean Satisfiability Solver”, Proceedings of International Conference...
  • M-MACBETH

  • Referenced in 104 articles [sw16199]
  • decision maker or a decision-advising group quantify the relative attractiveness of options. It employs...
  • FOCI

  • Referenced in 62 articles [sw12868]
  • prover. FOCI is a decision procedure for quantifier-free first-order formulas. It supports certain ... arrays. Most importantly, it can compute quantifier-free Craig interpolants for inconsistent pairs (or more...
  • RSOLVER

  • Referenced in 74 articles [sw04334]
  • RSolver is a program for solving quantified inequality constraints. Problems like projecting the solution...
  • DISCOVERER

  • Referenced in 58 articles [sw07719]
  • polynomial equations and polynomial inequalities. Algorithms for quantifier elimination of real closed fields...
  • UCPOP

  • Referenced in 39 articles [sw20687]
  • actions that have conditional effects and universally quantified preconditions and effects. It accepts universally quantified...
  • KeYmaera

  • Referenced in 48 articles [sw03709]
  • complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy...
  • DepQBF

  • Referenced in 46 articles [sw09734]
  • DepQBF is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal...
  • LabelMe

  • Referenced in 46 articles [sw36633]
  • over a wide variety of images. We quantify the contents of the dataset and compare...
  • STP

  • Referenced in 44 articles [sw34795]
  • constraint solver for the theory of quantifier-free bitvectors that can solve many kinds...
  • Bloqqer

  • Referenced in 31 articles [sw09578]
  • Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural...
  • leanTAP

  • Referenced in 41 articles [sw09985]
  • extended to the case of quantified modal logics as long as the Barcan formula...
  • QUBOS

  • Referenced in 25 articles [sw09580]
  • QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. We describe QUBOS (QUantified BOolean Solver ... decision procedure for quantified Boolean logic. The procedure is based on nonclausal simplification techniques that...
  • SQEMA

  • Referenced in 40 articles [sw03056]
  • Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided...