Name
Abstract | ||
|---|---|---|
We report advances in state-of-the-art algorithms for the problem of Minimal Unsatisfiable Subformula (MUS) extraction. First, we demonstrate how to apply techniques used in the past to speed up resolution-based Group MUS extraction to plain MUS extraction. Second, we show that model rotation, presented in the context of assumption-based MUS extraction, can also be used with resolution-based MUS extraction. Third, we introduce an improvement to rotation, called eager rotation. Finally, we propose a new technique for speeding-up resolution-based MUS extraction, called path strengthening. We integrated the above techniques into the publicly available resolution-based MUS extractor HaifaMUC, which, as a result, now outperforms leading MUS extractors. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1109/FMCAD.2013.6679410 | Formal Methods in Computer-Aided Design |
Keywords | Field | DocType |
computability,group theory,HaifaMUC,assumption-based MUS extraction,eager rotation,minimal unsatisfiable subformula,model rotation,path strengthening,resolution-based Group MUS extraction,resolution-based MUS extraction | Computer science,Algorithm,Computability,Extractor,Speedup | Conference |
Citations | PageRank | References |
16 | 0.60 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alexander Nadel | 1 | 213 | 13.95 |
| Vadim Ryvchin | 2 | 75 | 5.68 |
| Ofer Strichman | 3 | 1071 | 63.61 |