iSAT

| Beteiligte Mitarbeiter | Kooperationspartner | Beschreibung | Benchmarks | Publikationen |

iSAT wurde entwickelt, um die Lösbarkeit von Formeln bestehend aus Booleschen Verknüpfungen arithmetischer Constraints (einschliesslich transzendenten Funktionen) über reellwertigen Variablen zu prüfen. Dazu werden von iSAT aktuelle Techniken DPLL-basierter SAT-Solver genutzt (Lazy Clause Evaluation, konfliktgetriebenes Lernen, nichtchronologisches Backtracking und Restarts) und mit Interval-based Arithmetic Constraint Solving (ICP) kombiniert. Bei diesem Ansatz wird die Propagation der Arithmetischen Constraints direkt vom SAT Solver kontrolliert, während andere Ansätze aus dem Bereich des Lazy-Theorem-Proving arithmetische Entscheidungen durch einen nachgelagerten Solver bearbeiten lassen. Diese enge Verbindung zwischen DPLL und ICP in iSAT, ermöglicht es viele der algorithmischen Verbesserungen aus dem SAT Solver Bereich zu übernehmen. Dadurch ist es möglich auch mit sehr großen Problemen umzugehen -- insbesondere Problemen mit einem extrem komplexen Booleschen Anteil sowie Booleschen Kombinationen tausender arithmetischer Constraints. Zudem bietet iSAT auch ein BMC-Interface und kann somit die Gültigkeit von Eigenschaften bei Hybriden Systemen prüfen. Weitere Informationen sind unter http://projects.informatik.uni-freiburg.de/projects/isat/ und http://www.avacs.org/tools/isat/ zu finden. Anmerkung: iSAT ist der Nachfolger von HySAT und hat selbst einen Nachfolger: iSAT3.

Der iSAT Quickstart Guide gibt eine kurze Einführung in die Eingabesprache von iSAT.