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

SAT-Solver MIRA

| Beteiligte Mitarbeiter | Projektbeschreibung | Publikationen |


Beteiligte Mitarbeiter

ehemaliger Mitarbeiter Lehrstuhl ür Rechnerarchitektur
Matthew Lewis, Dr. Entwickler


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.



Publikationen
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