Name
Abstract | ||
|---|---|---|
Recently a new technique for improving algorithms for extracting Minimal Unsatisfiable Subsets (MUSes) from unsatisfiable CNF formulas called "model rotation" was introduced [Marques-Silva et. al. SAT2011]. The technique aims to reduce the number of times a MUS finding algorithm needs to call a SAT solver. Although no guarantees for this reduction are provided the technique has been shown to be very effective in many cases. In fact, such model rotation algorithms are now arguably the state-of-the-art in MUS finding. This work analyses the model rotation technique in detail and provides theoretical insights that help to understand its performance. These new insights on the operation of model rotation lead to several modifications and extensions that are empirically evaluated. Moreover, it is demonstrated how such MUS extracting algorithms can be effectively parallelized using existing techniques for parallel incremental SAT solving. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-33558-7_49 | CP |
Keywords | Field | DocType |
model rotation technique,existing technique,model rotation lead,model rotation,sat solver,parallelizing mus finding,mus finding algorithm,model rotation algorithm,mus finding,new insight,new technique | Mathematical optimization,Computer science,Boolean satisfiability problem,Algorithm,Theoretical computer science | Conference |
Citations | PageRank | References |
9 | 0.51 | 19 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Siert Wieringa | 1 | 88 | 4.99 |