TUD Logo

TUD Startseite » ... » Fakultät Informatik » Forschung » Wissenschaftliche Vorträge

Fakultät Informatik

against racism

Wissenschaftliche Vorträge

Towards Next Generation Sequential and Parallel SAT Solvers

Verteidigung im Promotionsverfahren von Dipl.-Inf. Norbert Manthey (Institut für Künstliche Intelligenz, Professur Knowledge Representation and Reasoning)

1.12.2014, 13:00 Uhr, INF 1004 (Ratssaal)

This thesis focuses on improving the SAT solving technology. The improvements focus on two major subjects: sequential SAT solving and parallel SAT solving. To better understand sequential algorithms, the abstract reduction system Generic CDCL is introduced. With Generic CDCL, the soundness of solving techniques can be modeled. Next, the conflict driven clause learning algorithm is extended with the three techniques local look-ahead, local probing and all UIP learning that allow more global reasoning during search. These techniques improve the performance of the sequential SAT solver Riss. Then, the formula simplification techniques bounded variable addition, covered literal elimination and an advanced cardinality constraint extraction are introduced. By using these techniques, the reasoning of the overall SAT solving tool chain becomes stronger than plain resolution. When using these three techniques in the formula simplification tool Coprocessor before using Riss to solve a formula, the performance can be improved further. Due to the increasing number of cores in CPUs, the scalable parallel SAT solving approach iterative partitioning has been implemented in Pcasso for the multi-core architecture. Related work on parallel SAT solving has been studied to extract main ideas that can improve Pcasso. Besides parallel formula simplification with bounded variable elimination, the major extension is the extended clause sharing level based clause tagging, which builds the basis for conflict driven node killing. The latter allows to better identify unsatisfiable search space partitions. Another improvement is to combine scattering and look-ahead as a superior search space partitioning function. In combination with Coprocessor, the introduced extensions increase the performance of the parallel solver Pcasso. The implemented system turns out to be scalable for the multi-core architecture. Hence iterative partitioning is interesting for future parallel SAT solvers. The implemented solvers participated in international SAT competitions. In 2013 and 2014 Pcasso showed a good performance. Riss in combination with Coprocessor won several first, second and third prices, including two Kurt-Gödel-Medals. Hence, the introduced algorithms improved modern SAT solving technology.


Die digitale Zeitung - Konzepte zur gebrauchstauglichen Gestaltung von digitalen Nachrichteninterfaces

Präsentation der Diplomarbeit (alle Studiengänge) von Thomas Schmalenberger (Institut für Software und Multimediatechnik; Professur für Mediengestaltung)

2.12.2014, 10:00 Uhr, INF 2101 Beratungsraum 2. Etage

Die Zeitungslandschaft befindet sich im Umbruch. Klassische Tageszeitungen verlieren seit Jahren an Auflage und Reichweite, während sinnvolle Konzepte zur Bekämpfung dieser Entwicklungen bislang fehlen. Die Verlage wirken rückläufigen Umsätzen mit Konzentrationsprozessen und Kosteneinsparungen entgegen. Zudem existieren kaum innovative Ansätze zur Transformation der gedruckten Zeitung in digitale Modelle. Redaktionelle Inhalte werden fast ausnahmslos in möglichst zeitungsähnlicher Weise als webbasiertes Angebot oder in Form von mobilen Apps präsentiert. Die Inhalte werden dabei meist unverändert wiederverwendet, eine Adaption an das digitale Medium oder gar den Leser findet nicht statt. Daraus ergibt sich die Grundthese der vorliegenden Arbeit: Den Lesern digitaler Nachrichtenplattformen fehlen geeignete Instrumente zur Navigation im Datenraum und zur Filterung der redaktionellen Inhalte.

Auf einem interdisziplinären Fundament wurden daher grundlegende Forderungen an die Funktion, die Struktur und die Gestaltung digitaler Zeitungen formuliert und in einem Prototypen zur abschließenden Evaluation umgesetzt. Das Ziel bestand dabei in der Transformation des Wesens der traditionellen Zeitung zu einem interaktiven Explorationswerkzeug, das sich dem Leser abhängig seiner Bedürfnisse und Gewohnheiten anpasst und ihm so einen mehrdimensionalen Zugang zur Datenbasis der redaktionellen Inhalte gewährt. Die Forderungen wurden losgelöst von technischen Rahmenbedingungen aufgestellt und beziehen sich auf jede Form der digitalen Veröffentlichung von tagesaktuellen Nachrichten.


Enhancements of the massively parallel memory allocator ScatterAlloc and its adaption to the general interface mallocMC

Präsentation der Studienarbeit (Großer Beleg) (alle Studiengänge) von Carlchristian Eckert (Institut für Technische Informatik, Professur Rechnerarchitektur)

2.12.2014, 13:00 Uhr, APB 1096

This work presents mallocMC, a general interface for memory allocation on accelerator devices. The policy based design of mallocMC enables a modular replacement of functional components as well as
configuration of the allocator at compile time. To provide a real world example for CUDA-capable accelerators, the existing high-performance memory allocator ScatterAlloc was adapted to mallocMC.
This adaption was enhanced with additional features and bugfixes and is expected to replace the current memory allocator in the massively parallel particle simulation PIConGPU.

Diese Veranstaltung wird unterstützt von Professur für Rechnerarchitektur.



Suche im Ankündigungsarchiv


Abonnieren Sie die Vortragsankündigungen als News Feed: RSS

Stand: 28.11.2014, 17:28 Uhr
Autor: Webmaster