PaQuBE

 

Subproject

S1

Categories

Core algorithms

Overview

PaQuBE is the parallel version of QuBE, a state-of-the-art Quantified Boolean Formula (QBF) solver. The parallelization makes use of the Message Passing Interface (MPI), and has a Master/Slave architecture.

Publications

M. Lewis, P. Marin, T. Schubert, M. Narizzano, B. Becker, E. Giunchiglia. Parallel QBF Solving with Advanced Knowledge Sharing. In Fundamenta Informaticae, Volume 107, Number 2-3, 139-166, 2011.

M. Lewis, P. Marin, T. Schubert, M. Narizzano, B. Becker, and E. Giunchiglia. PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing. In Oliver Kullmann, editor, Proceedings of SAT, International Conference on Theory and Applications of Satisfiability Testing, volume 5584 of Lecture Notes in Computer Science (LNCS), pages 509-523, 2009.

P. Marin, M. Lewis, T. Schubert, M. Narizzano, B. Becker, and E. Giunchiglia. Comparison of Knowledge Sharing Strategies in a Parallel QBF Solver. In High Performance Computing & Simulation Conference (HPCS), 2009.

Benchmarks

QBFLIB

Download

PaQuBE requires MPICH¹ libraries and environment to run correctly. Due to its specific requirements (paths, environment variables and daemons, ...) we do not provide a binary of PaQuBE.

¹ MPICH is an implementation of the "Message Passing Interface" standard.

Manual

---

Status

Prototype