QMiraXT

| project staff | description | benchmarks | publications |

This was the first modern parallel QBF solver with knowledge sharing. QMiraXT is a DPLL searched based solver that is inherits much of the framework introduced in the multi-threaded SAT solver MiraXT. QMiraXT introduced novel ideas on how to port many of the new advance techniques used in SAT solvers, into the QBF domain. It supported advanced forms of conflict and solution analysis with conflict clause learning. Furthermore, QMiraXT largest contribution was the introduction of the Single Quantification Level Scheduling algorithm for parallel QBF solvers that allowed it to efficiently divide large QBF problems into multiple smaller ones. This allowed QMiraXT to achieve significantly higher levels of CPU utilization
than any previous parallel QBF solver. The work in QMiraXT was then continued in the solver PaQuBE.

Any Quantified Boolean Formula (QBF) in QDimacs format. QBFLIB is the official library of QBF formulas.