Solving Sat in a Distributed Cloud: A Portfolio Approach

We introduce a new parallel and distributed algorithm for the solution of the satisfiability problem. It is based on an algorithm portfolio and is intended to be used for servicing requests in a distributed cloud. The core of our contribution is the modeling of the optimal resource sharing schedule in parallel executions and the proposition of heuristics for its approximation. For this purpose, we reformulate a computational problem introduced in a prior work. The main assumption is that it is possible to learn optimal resource sharing from traces collected on past executions on a representative set of instances. We show that the learning can be formalized as a set coverage problem. Then we propose to solve it by approximation and dynamic programming algorithms based on classical greedy algorithms for the maximum coverage problem. Finally, we conduct an experimental evaluation for comparing the performance of the various algorithms proposed. The results show that some algorithms become more competitive if we intend to determine the trade-off between their quality and the runtime required for their computation.

Modern Cooperative Parallel SAT Solving

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