QMiraXT

 

Subproject

S1

Categories

Core algorithms

Overview

QMiraXT was the first multi-threaded QBF solver. It is based on the SAT solver MiraXT, and includes all the features of an advanced SAT solver, but modified for use in QBF. On industrial problems, such as the verification of incomplete designs, it provides leading edge performance. It also introduced the vastly superior search space splitting algorithm SQLS that allowed the parallel solver to achieve high levels of processor utilization.

Publications

M. Lewis, T. Schubert, and B. Becker. QMiraXT - A Multithreaded QBF Solver. In GI/ITG/GMM Workshop on Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen, 2009.

Benchmarks

QBFLIB

Download

Click here for the binary.

Manual

Just type ./QMiraXT on the command line to see how it can be used.

Status

Prototype