Abstracts
From parallel theorem proving to parallel SATsolving and back
Maria Paola Bonacina
(Università degli Studi di Verona)
[slides]
In this talk we touch upon selected discoveries and ideas in
parallel theorem proving, revisiting the key role played by
the ClauseDiffusion method in moving parallel reasoning from
the parallelization of inferences to the parallelization of
search, which is the dominating paradigm today. We explore
both historic and conceptual connections between parallel
theorem proving and parallel satisfiability solving, and
envision the potential for new forays in parallel modelbased
theorem proving. No less surprising are the connections
between parallel reasoning and sequential settings that
nonetheless require the cooperation of inference systems,
such as satisfiability modulo combinations of theories.
Parallel Answer Set Programming
Andrea Formisano
(Università di Perugia)
[slides]
In this talk we explore the main techniques and approaches presented
in the literature and aimed at enabling the use of parallelism in
Answer Set Programming solvers.
This survey explores the approaches along two dimensions:
(1) one dimension is the underlying language, ranging from Datalog to full ASP;
(2) the second dimension is the granularity of parallelism, from
finegrained GPUbased parallelism to very large grained parallelism on
distributed platforms.
Parallel QBF Solving: State of the Art Techniques and Future Perspectives
Florian Lonsing
(TU Wien)
[slides]
Quantified Boolean formulas (QBF) are a formalism which extends propositional
logic by explicit existential or universal quantification of propositional
variables. Due to the PSPACEcompleteness of the QBF satisfiability problem,
QBFs are naturally applicable to encode problems from the complexity class
PSPACE or from any subclasses in the polynomial hierarchy.
We review the development of parallel approaches to solve QBFs starting from
its origins in the early 2000s. Although there has been considerable
inspiration by related techniques from parallel SAT solving, parallel QBF
solving has received relatively little attention compared to SAT. One reason
for this phenomenon is the presence of nested quantifiers in QBFs. The
resulting quantifier ordering imposes limitations on the way how parallel
computing resources can be exploited and complicates the implementation of
robust parallel QBF solvers.
From a general perspective, parallel QBF solving has considerable
potential. In contrast to sequential SAT solving, where conflictdriven clause
learning (CDCL) is omnipresent in state of the art solvers, for sequential QBF
solving there exist different solving paradigms with individual
strengths. That variety in the sequential QBF solver landscape opens promising
directions to improve the state of the art of parallel QBF solving.
Solving very hard problems: CubeandConquer, a hybrid SAT solving method
Marijn Heule
(University of Texas at Austin)
[slides]
Many search problems, from artificial intelligence to combinatorics, explore
large search spaces to determine the presence or absence of a certain object.
These problems are hard due to combinatorial explosion, and have traditionally
been called infeasible. The bruteforce method, which at least implicitly
explores all possibilities, is a general approach to search systematically
through such spaces. Brute force has long been regarded as suitable only for
simple problems. This has changed in the last two decades, due to the progress
in satisfiability (SAT) solving, which renders brute force into a powerful
approach to deal with many problems easily and automatically.
We illustrate the strength of SAT via the Boolean Pythagorean Triples problem,
which has been a longstanding open problem in Ramsey Theory. Our parallel SAT
solver allowed us to solve the problem on a cluster in about two days using 800
cores, demonstrating its linear time speedup on many hard problems. Due to the
general interest in this mathematical problem, our result requires a formal
proof. Exploiting recent progress in unsatisfiability proof checking, we
produced and verified a clausal proof of the smallest counterexample, which is
almost 200 terabytes in size. These techniques show great promise for attacking
a variety of challenging problems arising in mathematics and computer science.
Parallel Modelbased Diagnosis on MultiCore Computers
Dietmar Jannach
(TU Dortmund)
[slides]
ModelBased Diagnosis (MBD) is a principled and domainindependent way
of analyzing why a system under examination is not behaving as expected.
Given an abstract description (model) of the system's components and
their behavior when functioning normally, MBD techniques rely on
observations about the actual system behavior to reason about possible
causes when there are discrepancies between the expected and observed
behavior.
Due to its generality, MBD has been successfully applied in a variety of
application domains over the years. In many cases, constraint reasoning
is used simulate the system's behavior and to test different hypotheses
about the reasons for an observed failure. Despite the advances in
constraint reasoning, the generation of diagnoses can be computationally
challenging because traditional diagnosis algorithms do not exploit the
capabilities of modern multicore computers. In this talk I will discuss
different recently proposed schemes of parallelizing the diagnostic
reasoning process and present the results of a series of empirical
evaluations for different application scenarios.
Concurrent Data Structures for MultiCore Model Checking
Alfons Laarman (Universiteit Leiden)
[slides]
Model checking was long considered to require too much memory bandwidth
for efficient parallelization on modern multicores. Novel concurrent
data structures, however, have shown that the procedure can scale
linearly and often ideally up to at least 64 cores. The corner stone of
this solution is a concurrent hash table, which was carefully designed
to maximize locality and minimize contention. We discuss how this design
has since been used to parallelize stateoftheart compression
techniques in binary trees and decision diagrams (BDDs and MDDs).
P3: Model Checking using distributed PDR
Matteo Marescotti
(Università della Svizzera italiana)
[slides]
Property Directed Reachability (PDR) is an efficient model checking technique.
However, real world verification problems are often too hard, causing PDR
solvers to fail. Since sequential CPU speed has stopped growing and solvers are
already highly optimized, parallelization is the next logical direction.
However, this area of research is still poorly investigated. This talk
introduces P3 (Parallelly Performed PDR), an algorithm that enhances the power
offered by three distinct parallel techniques for PDR with the aim of exploiting
the massive computational power offered by distributed computing environments.
The involved techniques are 1) partitioning of the input problem, 2) exchanging
of learned reachability information, and 3) algorithm portfolios. We implemented
P3 using the SMTbased model checker Spacer and experimented over SVCOMP
benchmarks. Our experimentation shows up to an order of magnitude speedup and
twice as many instances solved within a timeout with respect to the sequential
implementation.
Harnessing over a Million CPU Cores to Solve a Single Hard Mixed Integer Programming Problem on a Supercomputer
Yuji Shinano
(Zuse Institute Berlin)
[slides]
Mixed integer programming (MIP) is a general form to model combinatorial
optimization problems and has many industrial applications. The
performance of MIP solvers, software packages to solve MIPs, has
improved tremendously in the last two decades and these solvers have
been used to solve many realword problems. However, against the
backdrop of modern computer technology, parallelization is of pivotal
importance. In this way, ParaSCIP is the most successful parallel MIP
solver in terms of solving previously unsolvable instances from the
wellknown benchmark instance set MIPLIB by using supercomputers. It
solved two instances from MIPLIB2003 and 12 from MIPLIB2010 for the
first time to optimality by using up to 80,000 cores of supercomputers.
Additionally, a specialized version of ParaSCIP for solving Steiner tree
problems called SCIPJack solved three open instances from the Steiner
tree test benchmark set PUC. ParaSCIP has been developed by using the
Ubiquity Generator (UG) framework, which is a general software package
to parallelize any stateoftheart branchandbound based solvers. The
UG framework is currently being used to develop ParaXpress, a
distributed memory parallelization of the commercial MIP solver Xpress.
Moreover, it is being used to parallelize PIPSSBB, a solver for
stochastic MIPs. Since Xpress is a multithreaded solver and ParaSCIP
can run at least 80,000 processes in parallel for solving a single MIP,
ParaXpress could handle over a million CPU cores. Furthermore, the
parallelization of PIPSSBB by the UG framework has the potential to
also handle over a million CPU cores. In this talk, a ground design of
the UG framework and its latest extensions to harness over a million CPU
cores will be presented and preliminary computational results will be
provided.
Parallel SAT Solving: Past, Present and Future
Carsten Sinz
(Karlsruhe Institute of Technology)
[slides]
In this talk we will give an overview of the history of parallelization
approaches for SAT solvers, ranging from techniques like guidingpaths in DPLL
to diversification and lemma exchange in recent parallel solvers. We will also
review theoretical limits of parallelizability and some effects that can be
observed in parallel solvers. The talk closes with an outlook on current
challenges and upcoming techniques.
