Topic Cardinality Resolution in Unsatisfiability Proofs

Studienarbeiten

• Themenvorschläge für Studien- und Abschlussarbeiten
• Abgeschlossene Arbeiten
  • Algebra und Diskrete Strukturen
  • Algebraische und logische Grundlagen der Informatik
  • Automatentheorie
  • Computational Logic
  • Knowledge-aware Artificial Intelligence
  • Logische Programmierung und Argumentation
  • Wissensbasierte Systeme
• Laufende Studienarbeiten

Toggle side column

Kardinalitätsresolution in Beweisen zur Unerfüllbarkeit

Verfügbar als Thema einer Bachelorarbeit, Masterarbeit, Diplomarbeit, Studienarbeit

•   Betreuer Tobias Philipp
•   Wissensverarbeitung
•   Beginn

The satisfiability problem (SAT) is one of the most prominent problems in theoretical computer science and has many applications in software verification, planning, bioinformatics or scheduling. Satisfiability solvers have become more complex in recent years due to inprocessing techniques and parallel computing. This raises the question whether the results of these solvers can be trusted. To gain confidence in the correctness of the results, SAT solvers can emit unsatisfiability proofs that can be validated using a checker.

Likewise, SAT solvers can detect cardinality constraints in the input formula, and perform specific reasoning procedures such as cardinality resolution. Such additional reasoning procedures significantly improve the efficiency of SAT solvers in certain domains. However, it is an open question how how one can construct unsatisfiability proofs in the DRAT proof format when the solver performs cardinality resolution