Home : QuBE, more than a QBF solver.
QuBE is an efficient search-based solver for Quantified Boolean Formulas (QBFs).
In computational complexity theory, the quantified Boolean formula satisfiability problem is a generalization of the Boolean satisfiability problem in which both existential quantifiers and universal quantifiers can be applied to each variable. QBF is the canonical complete problem for PSPACE, the class of problems solvable by a deterministic or nondeterministic Turing machine in polynomial space and unlimited time.
Deciding the satisfiability of QBFs is an important issue in Artificial Intelligence. Many reasoning tasks involving Planning (Synthesis), Abduction, Reasoning about Knowledge, non Monotonic Reasoning and Hardware Verification can be directly mapped into the problem of deciding the satisfiability of a QBF.
QuBE uses lazy data structures both for unit clauses propagation and for pure literals detection. It also features non-chronological backtracking, learning and a branching heuristic that leverages the information gathered during the backtracking phase.
QuBE reads formulas in QDimacs format, an extension of the Dimacs format for SAT and it returns the value of the formula, i.e., TRUE if the formula is satisfiable, and FALSE otherwise. QuBE6.0 is a composition of two different tools: (i) QuBE3.1 is an improvement of QuBE5.0 that participated at the 2006 qbf-competition, and a powerful preprocessor. QuBE6.0 (aka ncQuBE1.0 in QBFLIB) participated (with a good ranking) at the last qbf-competition. QuBE6.0 could be considered as an enhancement of QuBE5.0 that participated at the first qbf-competition (2006)
If you want to have more information about QuBE, or if you have suggestions about it, mail to:
qube_AT_star.dist.unige.it