SAT-Solver MIRA

| Beteiligte Mitarbeiter | Projektbeschreibung | Publikationen |

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.