
Quaffle
 Referenced in 63 articles
[sw07278]
 Quaffle: Quantified Boolean Formula Evaluator with Learning Quaffle is an experimental QBF solver. The idea ... Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver”, Proceedings of 8th International Conference...

QUBE
 Referenced in 29 articles
[sw11381]
 QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability. Deciding the satisfiability of a Quantified...

DepQBF
 Referenced in 31 articles
[sw09734]
 searchbased solver for quantified boolean formulae (QBF) in prenex conjunctive normal form...

QuBE++
 Referenced in 28 articles
[sw00766]
 describe QuBE++, an efficient solver for Quantified Boolean Formulas (QBFs). To the extent...

Bloqqer
 Referenced in 27 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...

semprop
 Referenced in 17 articles
[sw28383]
 model caching in decision procedures for quantified Boolean formulas. The increasing role of quantified Boolean ... selection in semantic tree procedures for quantified Boolean formulas, learning methods are more important than...

QBFLIB
 Referenced in 17 articles
[sw09581]
 Quantified Boolean formulas satisfiability library (QBFLIB). QBFLIB is a collection of instances, solvers, and tools ... related to Quantified Boolean Formula (QBF) satisfiability. QBFLIB is meant as a service...

Quantor
 Referenced in 22 articles
[sw28381]
 SATeLite. Quantor is a solver for quantified boolean formulas (QBF) in the QDIMACS format. Checking...

Nenofex
 Referenced in 18 articles
[sw09579]
 paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form ... eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes...

MPIDepQBF
 Referenced in 4 articles
[sw18671]
 present a lightweight approach for solving quantified Boolean formulas (QBFs) in parallel. In particular...

QUBOS
 Referenced in 24 articles
[sw09580]
 quantified Boolean logic. The procedure is based on nonclausal simplification techniques that reduce formulae...

HQSpre
 Referenced in 2 articles
[sw28634]
 tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified ... Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding socalled ... Henkinquantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed...

Squolem
 Referenced in 3 articles
[sw09453]
 Validating QBF invalidity in HOL4. The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates...

HordeQBF
 Referenced in 2 articles
[sw18670]
 core. We integrated the QCDCLbased quantified Boolean formula (QBF) solver DepQBF in HordeSAT...

ToyElim
 Referenced in 3 articles
[sw09900]
 equivalent formula without these operators. Tasks like elimination of Boolean quantifiers, computation of uniform interpolants ... solving, and processing of formulas according to various semantics of logic programming can be expressed...

SMCHR
 Referenced in 2 articles
[sw09322]
 with a modern Boolean satisfiability (SAT) solver for quantifierfree formulae with an arbitrary propositional...

Beaver
 Referenced in 9 articles
[sw00071]
 solver (theorem prover) for the theory of quantifierfree finiteprecision bitvector arithmetic ... Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich ... nonlinear arithmetic) and equivalence checking (rich Boolean structure...

DDDLIB
 Referenced in 1 article
[sw00192]
 constructing formulae with the standard Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding...

STABLE
 Referenced in 2 articles
[sw11913]
 Boolean reasoning with computer algebra. This paper presents a new SMT solver, STABLE, for formulas ... quantifierfree logic over fixedsized bit vectors (QFBV). The heart of STABLE...

SONOLAR
 Referenced in 2 articles
[sw26291]
 Solver that solves quantifierfree fixedsize bitvector logic formulas. The solver supports ... blasting to translate bitvector constraints to a Boolean formula and lets a SAT solver decide...