Wyniki wyszukiwania - BazTech

Ograniczanie wyników

2 Fundamenta Informaticae

Znaleziono wyników: 2

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

Twelve Years of QBF Evaluations : QSAT Is PSPACE-Hard and It Shows

Marin P., Pulina L., Giunchiglia E., Narizzano M., Tacchella A.

Fundamenta Informaticae

2016

Vol. 149, nr 1/2

133--158

Twelve years have elapsed since the first Quantified Boolean Formulas (QBFs) evaluation was held as an event linked to SAT conferences. During this period, researchers have striven to propose new algorithms and tools to solve challenging formulas, with evaluations periodically trying to assess the current state of the art. In this paper, we present an experimental account of solvers and formulas with the aim to understand the progress in the QBF arena across these years. Unlike typical evaluations, the analysis is not confined to the snapshot of submitted solvers and formulas, but rather we consider several tools that were proposed over the last decade, and we run them on different formulas from previous QBF evaluations. The main contributions of our analysis, which are also the messages we would like to pass along to the research community, are: (i) many formulas that turned out to be difficult to solve in past evaluations, remain still challenging after twelve years, (ii) there is no single solver which can significantly outperform all the others, unless specific categories of formulas are considered, and (iii) effectiveness of preprocessing depends both on the coupled solver and the structure of the formula.

Parallel QBF Solving with Advanced Knowledge Sharing

Lewis M., Schubert T., Becker B., Marin P., Narizzano M., Giunchiglia E.

Fundamenta Informaticae

2011

Vol. 107, nr 2/3

139-166

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.