Name
Abstract | ||
|---|---|---|
A minimal unsatisfiable subformula (MUS) of a given CNF is a set of clauses which is unsatisfiable, but becomes satisfiable as soon as we remove any of its clauses. In practical scenarios it is often useful to know, in addition to the unsolvability of an instance, which parts of the instance cause the unsolvability. An approach is here proposed to the problem of automatic detection of such a subformula, with the double aim of finding quickly a small-sized one. We make use of an adaptive technique in order to rapidly select an unsatisfiable subformula which is a good approximation of a MUS. Hard unsatisfiable instances can be reduced to remarkably smaller problems, and hence efficiently solved, through this approach. |
Year | Venue | Keywords |
|---|---|---|
2000 | CP | smaller problem,satisfiability instances,finding minimal unsatisfiable subformulae,practical scenario,automatic detection,adaptive technique,double aim,hard unsatisfiable instance,unsatisfiable subformula,good approximation,minimal unsatisfiable subformula,satisfiability |
Field | DocType | ISBN |
Constraint satisfaction,Discrete mathematics,Search algorithm,Computer science,Satisfiability,Algorithm,Search tree | Conference | 3-540-41053-8 |
Citations | PageRank | References |
3 | 0.71 | 3 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Renato Bruni | 1 | 127 | 15.79 |
| Antonio Sassano | 2 | 604 | 60.84 |