Logo des Repositoriums

Auflistung nach Autor:in "Manthey, Norbert"

1 - 4 von 4
  • Textdokument
    Ausgezeichnete Informatikdissertationen 2014
    (2015) Angerer, Andreas; Auer, Christopher; Berkholz, Christoph; Bermbach, David; Bringmann, Karl; Cano, Estefania; Distler, Tobias; Gisbrecht, Andrej; Herrmann, Dominik; Hoffmann, Steve; Hufsky, Franziska; Kirchner, Elsa Andrea; Klambauer, Günter; Lanthaler, Markus; Lawonn, Kai; Lemmerich, Florian; Linden, Sven; Manthey, Norbert; Michels, Dominik L.; Mühlbach, Sascha; Reuter, Christian; Rieke, Jahn; Rohr, David; Sallinger, Emanuel; Samek, Wojciech; Schmidt, Melanie; Tauheed, Farhan; Tschuggnall, Michael; Wenger, Stephan; Ziller, Michael J.
  • Textdokument
    Modernes sequentielles und paralleles SAT Solving
    (Ausgezeichnete Informatikdissertationen 2014, 2015) Manthey, Norbert
    Das Lösen des Erfüllbarkeitsproblems (SAT) wird in vielen industriellen Anwendungen genutzt, zum Beispiel in der Verifikation von Hardware und Software oder beim Erstellen von Fahrplänen. Verbesserungen der SAT-Technologie wirken sich somit unmittelbar auf darauf aufbauende Anwendungen aus. In dieser Arbeit werden sequentielle SAT-Systeme modelliert und Erweiterungen für den Suchalgorithmus vorgestellt, sowie neue Vereinfachungstechniken vorgeschlagen. Da heutigen Rechenarchitekturen viele Rechenkerne beherbergen, wird weiterhin ein skalierbarer, paralleler Lösungsalgorithmus präsentiert. Alle diskutierten Algorithmen wurden implementiert und empirisch ausgewertet: Die vorgestellten Erweiterungen verbessern den Stand heutiger SAT-Technologie.
  • Zeitschriftenartikel
    SATPin: Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT
    (KI - Künstliche Intelligenz: Vol. 34, No. 3, 2020) Manthey, Norbert; Peñaloza, Rafael; Rudolph, Sebastian
    One approach to axiom pinpointing (AP) in description logics is its reduction to the enumeration of minimal unsatisfiable subformulas, allowing for the deployment of highly optimized methods from SAT solving. Exploiting the properties of AP, we further optimize incremental SAT solving, resulting in speedups of several orders of magnitude: through persistent incremental solving the solver state is updated lazily when adding clauses or assumptions. This adaptation consistently improves the runtime of the tool by an average factor of 3.8, and a maximum of 38. SATPin , our system, was tested over large biomedical ontologies and performed competitively.
  • Zeitschriftenartikel
    Towards Next Generation Sequential and Parallel SAT Solvers
    (KI - Künstliche Intelligenz: Vol. 30, No. 0, 2016) Manthey, Norbert