Abschlussarbeit

Bachelorarbeit „SAT-Kodierungen für Quasi-Inkonsistenz“

Verfasser/in:
Michael Annen
Ansprechperson:
Prof. Dr. Matthias Thimm
Status:
abgeschlossen
Jahr:
2022
Download:
Bachelor.Annen

Beschreibung:

Business Rules Management (BRM) [1] beschreibt die Erstellung, Pflege und Anwendung von sog. Geschäftsregeln zur Repräsentation der Geschäftslogik in Firmen. Mithilfe dieser Regeln können Prozesse transparent modelliert und insbesondere auf Einhaltung von Normen überprüft werden. Formal gesehen sind Geschäftsregeln Regeln der Form „Wenn A1,…,An dann B”. Gegeben einer konkreten Instanz zur Laufzeit (beispielsweise persönliche Informationen eines potentiellen Kunden eines Kreditantrags) werden die Regeln angewendet und entsprechende Schlussfolgerungen betrieben (beispielsweise die Genehmigung des Kreditantrags). Da die Menge der Geschäftsregeln üblicherweise recht groß und von vielen Mitarbeitern erstellt und gepflegt wird, können hier leicht bei konkreten Instanzen Inkonsistenzen auftreten (beispielsweise wird sowohl die Genehmigung als auch die Ablehnung des Kreditantrags gefolgert). Diese „potentiellen“ Inkonsistenzen können nicht mit klassischen Methoden der Inkonsistenzanalyse behandelt werden, stellen aber ein praktisch relevantes Problem dar. In [2] wird der Begriff der Quasi-Inkonsistenz eingeführt, der eine Formalisierung besonders relevanter solcher Probleme darstellt, und kompexitätstheoretisch untersucht.

In dieser Bachelorarbeit sollen die theoretischen Ergebnisse aus [1] genutzt werden, um einen Algorithmus zu entwerfen und zu implementieren, der Quasi-Inkonsistenz in Regelbasen erkennen kann. Da das Problem der Erkennung von Quasi-Inkonsistenz NP-vollständig ist [2], ist eine Kodierung des Problems als Satisfiability Problem [3] und eine Implementierung durch SAT-Solver naheliegend. In dieser Arbeit soll eine entsprechende SAT-Kodierung dazu entwickelt und mithilfe von SAT-Solvern implementiert werden.

  • [1] I. Graham, Business rules management and service oriented architecture: a pattern language, John wiley & sons, 2007.
  • [2] Carl Corea, Matthias Thimm. On Quasi-Inconsistency and its Complexity. In Artificial Intelligence, 284:103276. July 2020.
  • [3] Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (Editors). Handbook of Satisfiability. IOS Press, 2009.
09.04.2024