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

iSAT

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


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Karsten Scheibler, Dipl.-Inf. Entwickler
Tobias Schubert, Dr. Entwickler
Felix Neubauer, M.Sc. Entwickler / Kontakt
ehemalige Mitarbeiter Lehrstuhl für Rechnerarchitektur
Natalia Kalinnik, Dipl.-Inf. Entwickler
Stefan Kupferschmid, Dr. Entwickler
Kooperationspartner

ehemalige Mitarbeiter Universität Oldenburg
Andreas Eggers, Dr. Entwickler
Tino Teige, Dr. Entwickler
Universität Oldenburg
Ahmed Mahdi, M.Sc Entwickler


Beschreibung

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.



Benchmarks

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



Publikationen
Martin Fränzle, Christian Herde, Tino Teige, Stefan Ratschan, and Tobias Schubert
Efficient Solving of Large Non-Linear Arithmetic Constraint Systems with Complex Boolean Structure
Journal on Satisfiability, Boolean Modeling, and Computation, Volume 1 (2007), pages 209-236