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

Projekte

SAT-Solver MIRA

Projektbeschreibung

MIRA ist ein vollstaendiger Algorithmus zum Loesen des propositionalen SAT Problemes. Die Kernelemente - basierend auf Ideen von SAT-Prozeduren wie zChaff, Berkmin oder auch Siege - sind hierbei Konfliktanalyse, Watched Literals und diverse Heuristiken zur Auswahl der jeweils naechsten Entscheidungsvariablen. Aufbauend auf diesen (Standard-)Techniken wird MIRA durch weitergehende, leistungsfaehige Funktionen komplettiert: Implication Queue Sorting (IQS), Early Conflict Detection Based BCP (ECDB) sowie eine sich dynamisch anpassende Kombination der verschiedenen zur Verfuegung stehenden Auswahlheuristiken. Durch die Integration aller vorgenannter Strategien ist MIRA in der Lage, die benoetigte Rechenzeit zur Loesung zahlreicher Probleme (z.B. BMC-Benchmarks sowie andere Industrie-Benchmarks) erheblich zu reduzieren.

Laufzeit

01.01.2003 bis 31.12.2009

Projektleitung

Prof. Dr. Bernd Becker