Name
Abstract | ||
|---|---|---|
We introduce an algorithm for finding a minimal unsatisfiable subset (MUS) of a CNF formula. We have implemented and evaluated the algorithm and found that its performance is very competitive on a wide range of benchmarks, including both formulas that are close to minimal unsatisfiable and formulas containing MUSes that are only a small fraction of the formula size. In our simple but effective algorithm we associate assignments with clauses. The notion of associated assignment has emerged from our work on a Brouwer's fixed point approximation algorithm applied to satisfiability. There, clauses are regarded to be entities that order the set of assignments and that can select an assignment to be associated with them, resulting in a Pareto optimal agreement. In this presentation we abandon all terminology from this theory which is superfluous with respect to the recent objective and make the paper self contained. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1007/978-3-540-79719-7_27 | SAT |
Keywords | Field | DocType |
fixed point approximation algorithm,pareto optimal agreement,associated assignment,minimal unsatisfiable,formula size,cnf formula,minimal unsatisfiable subset,associate assignment,paper self,effective algorithm,satisfiability,fixed point | Discrete mathematics,Terminology,Computer science,Satisfiability,Binary decision diagram,Pareto optimal,Constraint satisfaction problem,Fixed point approximation | Conference |
Volume | ISSN | ISBN |
4996 | 0302-9743 | 3-540-79718-1 |
Citations | PageRank | References |
22 | 0.92 | 19 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hans van Maaren | 1 | 185 | 15.75 |
| Siert Wieringa | 2 | 88 | 4.99 |