HordeQBF: A Modular and Massively Parallel QBF Solver
This work addresses the challenge of efficiently solving QBF problems, which is important for applications in formal verification and AI, but it is incremental as it adapts an existing parallel SAT solver framework to QBF.
The authors tackled the problem of solving quantified Boolean formulas (QBF) by integrating the QCDCL-based solver DepQBF into the modular, massively parallel SAT solver HordeSAT to create HordeQBF, achieving superlinear average and median speedup on hard application instances from the 2014 QBF Gallery.
The recently developed massively parallel satisfiability (SAT) solver HordeSAT was designed in a modular way to allow the integration of any sequential CDCL-based SAT solver in its core. We integrated the QCDCL-based quantified Boolean formula (QBF) solver DepQBF in HordeSAT to obtain a massively parallel QBF solver---HordeQBF. In this paper we describe the details of this integration and report on results of the experimental evaluation of HordeQBF's performance. HordeQBF achieves superlinear average and median speedup on the hard application instances of the 2014 QBF Gallery.