SAT-Solver MIRA

| project staff | project description | publications |

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).