Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

Mira-Craig

| Beteiligte Mitarbeiter | Beschreibung |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Stefan Kupferschmid, Dipl.-Inf. Entwickler / Kontakt


Beschreibung

Die statisch gelinkte Library libcraigsolver.a stellt eine Schnittstelle zur Verfügung mit Hilfe derer Craigsche Interpolanten und sogenannte UNSAT Cores berechnet werden können. Die berechneten Interpolanten können in Konjunktiver Normalen Form (KNF) zurückgegeben werden, dazu wird die eigentliche Interpolante Tseitin-kodiert. Der in dieser Library enthaltene SAT Solver ist MiraXT.