Kardinalitätsresolution in Beweisen zur Unerfüllbarkeit

Thema nicht mehr verfügbar

Betreuer Tobias Philipp
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