Coprocessor
Aus International Center for Computational Logic
Coprocessor
Formelvereinfachungen für CNF (SAT), QBF, MaxSAT und MUS Formeln
- Kontaktperson Sibylle Möhle
- http://tools.computational-logic.org
- Veröffentlichungsdatum 1. Juli 2012
Coprocessor ist ein eigenständiges Werkzeug zur Formelvereinfachung für verschiedenen Probleme. Die meisten Techniken wurden für CNF Formeln entwickelt, die Optimierungsvariante MaxSAT wird aber ebenso unterstützt wie MUS. Ein Teil der Techniken kann auch für QBF verwendet werden. Coprocessor implementiert beinah alle veröffentlichten Vereinfachungstechniken. Zu den Vereinfachungen können Statistiken ausgegeben werden, außerdem kann die Reihenfolge der Techniken angegeben werden, und Variablen können von der Vereinfachung ausgeschlossen werden. Dadurch kann Coprocessor auch Formeln vereinfachen, für die nachher mehrere Modelle auf einer Untermenge ihrer Variablen generiert werden soll.
