Uni-Logo
Deutsch      
Computer Architecture - Team Bernd Becker
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

Projects

SAT-Solver MIRA

Project description

MIRA is a complete SAT solver that inherited first UIP conflict analysis, watched literal list, VSIDS, VMTF, and others features from solvers such as zChaff, Berkmin, and Siege. Building on these techniques, MIRA goes farther, implementing Implication Queue Sorting (IQS) and Early Conflict Detection Based BCP (ECDB) while also introducing an enhanced hybrid decision strategy. The inclusion of these elements into MIRA allows it to realize significant speedup in numerous problem instances (e.g. in BMC benchmarks as well as other industrial benchmarks).

Start/End of project

01.01.2003 until 31.12.2009

Project manager

Prof. Dr. Bernd Becker