Paper Info
Title
Parallel QBF Solving with Advanced Knowledge Sharing
Abstract
In 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 multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results.
Year
DOI
Venue
2011
10.3233/FI-2011-398
Fundam. Inform.
Keywords
Field
DocType
multiple conflict clause,parallel framework,knowledge sharing,parallel qbf,parallel qbf solver paqube,mpi message,solution cube,advanced knowledge sharing,previous generation solvers,advanced knowledge,progressive mpi,conflict clause,mpi
Knowledge sharing,Adaptive method,Computer science,Theoretical computer science,Bandwidth (signal processing),Solver,Cube
Journal
Volume
Issue
ISSN
107
2-3
0169-2968
Citations 
PageRank 
References 
4
0.42
36
Authors
6
Name
Order
Citations
PageRank
Matthew Lewis11076.37
Tobias Schubert259837.74
Bernd Becker385573.74
Paolo Marin4676.83
Massimo Narizzano545130.41
Enrico Giunchiglia62380164.28