The Hobel algorithm : SAT Lösung mit GPU über DPLL

Abstract

Das Erfüllbarkeitsproblem der Aussagenlogik (SAT, von englisch satisfiability-'Erfüllbarkeit') ist einer der wichtigsten NP-vollständiges Problem, das vielen Fällen in einer Vielzahl von Anwendungsgebieten im Bereich von Schaltung und Hardware-Design zu Rechensystembiologie finden. Trotz der Komplexität des Problems, sind moderne SAT Solver sehr ausgefeilte Werkzeuge, die Hunderttausende von Variablen und Millionen von Klauseln leicht verarbeiten kann. Eines der wirksamsten Verfahren SAT Probleme zu lösen, ist der Davis-Putnam-Logemann-Loveland (DPLL) -Algorithmus. DPLL ist eine Backtracking Suche auf Basis sequentieller Algorithmus und es ist weit verbreitet in den State-of-the-art-SAT-Solver. Mit dem Aufkommen der hochparallele Architekturen, das Interesse der Gemeinschaft SAT Solver hat in Richtung der Parallelisierung von sequentiellen Algorithmen wie DPLL bewegt, um die Vorteile der leistungsfähigen Verarbeitungsmöglichkeiten in den modernen Multicore-Hardware-Architekturen in Anspruch zu nehmen. In dieser Arbeit nähern wir uns der Herausforderung, aus einem anderen Blickwinkel effektiv parallel SAT Solver zu entwickeln. Anstatt einen Suchalgorithmus wie die meisten Löser zu verwenden, wir verarbeiten die Klauseln nacheinander. Der Algorithmus beschreibt die möglichen Modelle zu den bereits verarbeitet Klauseln. Wenn eine neue Klausel verarbeitet worden ist, werden die beschriebenen Modelle so modifiziert werden, so dass die neu verarbeitet Klausel zufrieden sein werden. Im Falle des Verfahrens, eine der wichtigsten Bedingungen war die Ausnutzung der GPU. Wir führen eine neue logische Darstellung ein und wir konzentrieren uns auf Single Instruction Multiple Data (SIMD). Verschiedene Art von Aufgaben wurden durchgeführt, die die GPU passen. Der Algorithmus wurde mit C ++ und CUDA implementiert. Die Tests wurden an einer NVIDIA Geforce GTX 860M Grafikkarte durchgeführt. Während der Entwicklung wurde der Algorithmus auf der Grundlage der Testergebnisse verbessert. Die Arbeit beschreibt die Grundidee und die wichtigsten Schritte dieser Verbesserungen mit den Testergebnissen.

The boolean satisfiability (SAT) is one of the most important NP-complete problem that find many instances in a large variety of application areas ranging from circuit and hardware design to computational systems biology. Despite the complexity of the problem, modern SAT solvers are very sophisticated tools that can easily handle hundred thousands of variables and millions of clauses. One of the most effective procedure to solve SAT problems is the Davis-Putnam-Logemann-Loveland (DPLL) algorithm. DPLL is a backtracking-search based sequential algorithm now widely employed in the state-of-the-art SAT solvers. With the advent of highly parallel architectures, the interest of the SAT solvers community has moved toward the parallelization of sequential algorithms such as DPLL to take advantage of the powerful processing capabilities offered in the modern multi-core hardware architectures. In this thesis we approach the challenge of developing effective parallel SAT solvers from a different point of view. Instead of use a search algorithm like most of the solvers, we process the clauses after each other. The algorithm describes the possible models to the already processed clauses. When a new clause has been processed, the described models will be modified so, such that the newly processed clause will be satisfied. In case of the procedure, one of the most important conditions was the utilization of the GPU. We introduce a new logical representation, and we concentrate on one single instruction multiple data (SIMD). Different sort of tasks have been performed which fit the GPU. The algorithm has been implemented with C++ and CUDA. The tests were performed on an NVIDIA Geforce GTX 860M graphics card. During the development, the algorithm has been improved based on the test results. The thesis describes the basic idea and the main steps of these improvements with test results.