A parallel portfolio SAT solver with lockless physical clause sharing

Abstract

Since multi-core architectures have become well-established the enquiry for parallel SAT solvers has drastically increased. Meanwhile, several successful SAT solvers have been presented that can be run in parallel mode. However, there are only a few solvers that use the shared memory architectures for physical clause sharing. In this paper we present a parallel SAT solver that allows for sharing clauses between several threads logically and physically. Yet any thread is still able to keep its own set of clauses. We show how physical clause sharing can be used to propagate one thread's improvements on the clause database to all solving threads. Despite the extensive sharing of data our solver does not require any operating system lock.