POS-13: Papers with Abstracts

Abstract. Preprocessing techniques are crucial for SAT solvers when it comes to reaching state-
of-the-art performance as it was shown by the results of the last SAT Competitions. The
usefulness of a preprocessing technique depends highly on its own parameters, on the in-
stances on which it is applied and on the used solver. In this paper we first give an extended
analysis of the performance gain reached by using different preprocessing techniques in-
dividually in combination with CDCL solvers on application instances and SLS solvers
on crafted instances. Further, we provide an analysis of combinations of preprocessing
techniques by means of automated algorithm configuration, where we search for optimal
preprocessor configurations for different scenarios. Our results show that the performance
of CDCL and especially of SLS solvers can be further improved when using appropriate
preprocessor configurations. The solvers augmented with the best found preprocessing
configurations outperform the original solvers on the instances from the SAT Challenge
2012, achieving new state-of-the-art results.

Abstract. Car sequencing is a well known NP-complete problem. This
paper introduces encodings of this problem into CNF based on sequential
counters. We demonstrate that SAT solvers are powerful in this domain
and report new lower bounds for the benchmark set in the CSPlib.

Abstract. Effectively parallelizing SAT solving is an open and
important issue. The current state-of-the-art is
based on parallel portfolios. This technique relies
on running multiple solvers on the same instance in
parallel. As soon one instance finishes the entire
run stops. Several succesful systems even use plain
parallel portfolio (PPP), where the individual solvers
do not exchange any information. This paper contains
a thorough experimental evaluation which shows that PPP
can improve wall-clock running time because memory access
is still local, respectively the memory system can hide
the latency of memory access. In particular, there does
not seem as much cache congestion as one might imagine.
We also present some limits on the scalibility of PPP.
Thus this paper gives one argument why PPP solvers are a
good fit for todays multi-core architectures.

Abstract. Nowadays, powerful parallel SAT solvers are based on an algorithm portfolio. The
alternative approach, (iterative) search space partitioning, cannot keep up, although, ac-
cording to the literature, iterative partitioning systems should scale better than portfolio
solvers. In this paper we identify key problems in current parallel cooperative SAT solving
approaches, most importantly communication, how to partition the search space, and how
to utilize the sequential search engine. First, we improve on each problem separately. In
a further step, we show that combining all the improvements leads to a state-of-the-art
parallel SAT solver, which does not use the portfolio approach, but instead relies on it-
erative partitioning. The experimental evaluation of this system completely changes the
picture about the performance of search space partitioning SAT solvers: on instances of
a combined benchmark of recent SAT competitions, the presented approach can keep up
with the winners of last years SAT competition. The combined improvements improve the
existing cooperative solver splitter by 24%: instead of 561 out of 880 instances, the new
solver Pcasso can solve 696 instances.