|
|
POS-13: Papers with AbstractsPapers |
---|
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. |
|
|
|