SAT-Solver MIRA
| Beteiligte Mitarbeiter | Projektbeschreibung | Publikationen
|
| ehemaliger Mitarbeiter Lehrstuhl ür Rechnerarchitektur | |
| Matthew Lewis, Dr. | Entwickler |
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.
|
Matthew Lewis, M.Sc.(Eng), Tobias Schubert, Dr., Bernd Becker, Prof. Dr. Early Conflict Detection Based BCP for SAT Solving 7th International Conference on Theory and Applications of Satisfiability Testing, 2004 |
|
Matthew Lewis, M.Sc.(Eng), Tobias Schubert, Dr., Bernd Becker, Prof. Dr. Speedup Techniques utilized in Modern SAT Solvers - An Analysis in the MIRA Environment 8th International Conference on Theory and Applications of Satisfiability Testing, 2005 |