Universität zu Köln

Grinten, Alexander van der (2017). Design, implementation and evaluation of a distributed CDCL framework. PhD thesis, Universität zu Köln.

Preview

PDF thesis.pdf - Published Version Download (956kB)

Abstract

The primary subject of this dissertation is practically solving instances of the Boolean satisfiability problem (SAT) that arise from industrial applications. The invention of the conflict-driven clause-learning (CDCL) algorithm led to enormous progress in this field. CDCL has been augmented with effective pre- and inprocessing techniques that boost its effectiveness. While a considerable amount of work has been done on applying shared-memory parallelism to enhance the performance of CDCL, solving SAT on distributed architectures is studied less thoroughly. In this work, we develop a distributed, CDCL-based framework for SAT solving. This framework consists of three main components: 1. An implementation of the CDCL algorithm that we have written from scratch, 2. a novel, parallel SAT algorithm that builds upon this CDCL implementation and 3. a collection of parallel simplification techniques for SAT instances. We call our resulting framework satUZK; our parallel solving algorithm is called the distributed divide-and-conquer (DDC) algorithm. The DDC algorithm employs a parallel lookahead procedure to dynamically partition the search space. Load balancing is used to ensure that all computational resources are utilized during lookahead. This procedure results in a divide-and-conquer tree that is distributed over all processors. Individual threads are routed through this tree until they arrive at unsolved leaf vertices. Upon arrival, the lookahead procedure is invoked again or the leaf vertex is solved via CDCL. Several extensions to the DDC algorithm are proposed. These include clause sharing and a scheme to locally adjust the LBD score relative to the current search tree vertex. LBD is a measure for the usefulness of clauses that participate in a CDCL search. We evaluate our DDC algorithm empirically and benchmark it against the best distributed SAT algorithms. In this experiment, our DDC algorithm is faster than other distributed, state-of-the-art solvers and solves at least as many instances. In addition to running a parallel algorithm for SAT solving we also consider parallel simplifcation. Here, we first develop a theoretical foundation that allows us to prove the correctness of parallel simplification techniques. Using this as a basis, we examine established simplification algorithms for their parallelizability. It turns out that several well-known simplification techniques can be parallelized efficiently. We provide parallel implementation of the techniques and test their effectiveness in empirical experiments. This evaluation finds several combinations of simplification techniques that can solve instances which could not be solved by the DDC algorithm alone.

Item Type:	Thesis (PhD thesis)
Translated abstract:	Abstract Language Im Kern beschäftigt sich diese Dissertation mit dem praktischen Lösen des Erfüllbarkeitsproblems der Aussagenlogik (SAT). Die Probleminstanzen, um die es dabei geht, stammen aus industriellen Anwendungen. Die Entdeckung des Conflict-Driven Clause-Learning (CDCL) Algorithmus führte zu enormen Fortschritten in diesem Bereich. CDCL wurde durch effektive Pre- und Inprocessingtechniken erweitert, welche die Leistungsfähigkeit des Algorithmus erhöhen. Während in der Vergangenheit viel Forschungsarbeit in den Einsatz von shared-memory Parallelität zum Beschleunigen von CDCL geflossen ist, blieb das Lösen von SAT auf verteilten Rechnern weniger gut erforscht. In dieser Arbeit entwickeln wir ein verteiltes, auf CDCL basierendes Framework, um SAT zu Lösen. Dieses Framework besteht hauptsächlich aus drei Komponenten: 1. Einer Implementierung des CDCL-Verfahrens, die wir von Grund auf neu geschrieben haben, 2. einem neuartigem Algorithmus um SAT mit Hilfe von Parallelität zu lösen, und 3. einer Ansammlung von parallelen Vereinfachungstechniken für SAT-Instanzen. Das entstandene Framework nennen wir satUZK, während der parallele Lösungsalgorithmus der Distributed Divide-and-Conquer (DDC) Algorithmus ist. DDC verwendet eine parallele Lookahead-Prozedur, um den Suchraum dynamisch zu zerteilen. Dabei wird Load Balancing genutzt um sicherzustellen, dass alle zur Verfügung stehenden Resourcen des verteilen Rechners ausgenutzt werden. Diese Prozedur erstellt einen Divide-and-Conquer Baum, der über alle Prozessoren verteilt wird. Individuelle Threads werden durch diesen Baum geleitet, bis sie ein ungelöstes Blatt erreichen. Bei Ankunft an einem Blatt wird entweder die Lookahead-Prozedur erneut aufgerufen oder das Blatt wird durch CDCL gelöst. Wir schlagen mehrere Erweiterungen für diesen Algorithmus vor. Insbesondere integrieren wir eine Strategie um Klauseln zwischen Threads austauschen und ein Schema, um den sogenannten LBD-Wert von Klauseln relativ zur lokalen Position im Suchbaum anzupassen. LBD ist ein Maß für die Nützlichkeit einer Klausel während der CDCL-Suche. Wir evaluieren unseren Algorithmus empirisch und messen ihn an den besten, verteilen SAT Algorithmen. In diesem Experiment ist unser Algorithmus schneller als andere, verteilte Solver und löst mindestens ebenso viele Instanzen. Zusätzlich zu dem parallelen Lösungsalgorithmus betrachten wir auch parallele Vereinfachungstechniken. Dabei entwickeln wir zunächst eine theoretische Grundlage, die es uns erlaubt, die Korrektheit von parallelen Vereinfachungstechniken nachzuweisen. Auf dieser Basis untersuchen wir etablierte Vereinfachungstechniken auf ihre Parallelisierbarkeit. Es stellt sich heraus, dass einige dieser Techniken sehr gut parallelisierbar sind. Für diese Techniken stellen wir parallele Implementierungen bereit, die wir empirisch auf ihre Effektivität hin untersuchen. Als Ergebnis dieser Untersuchung identifizieren wir mehrere Techniken, die es erlauben, Instanzen zu Lösen, die der DDC Algorithmus alleine nicht lösen kann. German
Creators:	Creators Email ORCID ORCID Put Code Grinten, Alexander van der vandergrinten@informatik.uni-koeln.de UNSPECIFIED UNSPECIFIED
URN:	urn:nbn:de:hbz:38-82810
Date:	20 November 2017
Language:	English
Faculty:	Faculty of Mathematics and Natural Sciences
Divisions:	Faculty of Mathematics and Natural Sciences > Department of Mathematics and Computer Science > Institute of Computer Science
Subjects:	Data processing Computer science
Uncontrolled Keywords:	Keywords Language SAT, CDCL, distributed solver, CNF simplification, preprocessing, inprocessing English
Date of oral exam:	16 January 2018
Referee:	Name Academic Title Speckenmeyer, Ewald Prof. Dr. Meyerhenke, Henning Prof. Dr.
Refereed:	Yes
URI:	http://kups.ub.uni-koeln.de/id/eprint/8281