A parallel portfolio SAT solver with lockless physical clause sharing

DSpace Repository


URI: http://nbn-resolving.de/urn:nbn:de:bsz:21-opus-55511
Dokumentart: Report
Date: 2011
Source: WSI ; 2011 ; 2
Language: English
Faculty: 7 Mathematisch-Naturwissenschaftliche Fakultät
Department: Informatik
DDC Classifikation: 004 - Data processing and computer science
Keywords: Multithreading , Erfüllbarkeitsproblem
Other Keywords: SAT , Parallel
SAT on multi-core , Algorithm engineering , Portfolio SAT solving
License: http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=de http://tobias-lib.uni-tuebingen.de/doku/lic_mit_pod.php?la=en
Order a printed copy: Print-on-Demand
Show full item record


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.

This item appears in the following Collection(s)