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