PaQuBE: Distributed QBF solving with advanced knowledge sharing. n this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multicore boxes to clusters and grids, to solve more relevant instances and faster than previous generation solvers. PaQuBE extends QuBE, its sequential core, by providing a Master/Slave Message Passing Interface (MPI) based design that allows it to split the problem up over an arbitrary number of distributed processes. Furthermore, PaQuBE’s progressive parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be shared. According to the last QBF Evaluation, QuBE is the most powerful state-of-the-art QBF Solver. It was able to solve more than twice as many benchmarks as the next best independent solver. Our results here, show that PaQuBE provides additional speedup, solving even more instances, faster.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Becker, Bernd; Ehlers, Rüdiger; Lewis, Matthew; Marin, Paolo: ALLQBF solving by computational learning (2012)
- Martins, Ruben; Manquinho, Vasco; Lynce, In^es: An overview of parallel SAT solving (2012)
- Hyvärinen, Antti E.J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning search spaces of a randomized search (2011)
- Teige, Tino; Eggers, Andreas; Fränzle, Martin: Constraint-based analysis of concurrent probabilistic hybrid systems: an application to networked automation systems (2011)
- Lewis, Matthew; Marin, Paolo; Schubert, Tobias; Narizzano, Massimo; Becker, Bernd; Giunchiglia, Enrico: PaQuBE: distributed QBF solving with advanced knowledge sharing (2009) ioport