Name
Abstract | ||
|---|---|---|
The paper is concerned with the relevant practical problem of selecting a small unsatisfiable subset of clauses inside an unsatisfiable CNF formula. Moreover, it deals with the algorithmic problem of improving an enumerative (DPLL-style) approach to SAT, in order to overcome some structural defects of such an approach. Within a complete solution framework, we are able to evaluate the difficulty of each clause by analyzing the history of the search. Such clause hardness evaluation is used in order to rapidly select an unsatisfiable subformula (of the given CNF) which is a good approximation of a minimal unsatisfiable subformula (MUS). Unsatisfiability is proved by solving only such subformula. Very small unsatisfiable subformulae are detected inside famous Dimacs unsatisfiable problems and in real-world problems. Comparison with the very efficient solver SATO 3.2 used as a state-of-the-art DPLL procedure (disabling learning of new clauses) shows the effectiveness of such enumeration guide. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1016/S0166-218X(02)00399-2 | Discrete Applied Mathematics |
Keywords | Field | DocType |
small unsatisfiable subformulae,unsatisfiable cnf formula,small unsatisfiable subset,consistency restoring,enumeration,unsatisfiability.,algorithmic problem,unsatisfiable subformula,adaptive core search,clause hardness evaluation,new clause,unsatisfiable problem,minimal unsatisfiable subformulae,real-world problem,(un)satisfiability,minimal unsatisfiable subformula,satisfiability | Algorithmics,Unsatisfiable core,Satisfiability,Boolean satisfiability problem,Algorithm,Conjunctive normal form,DPLL algorithm,Solver,Mathematics,Propositional formula | Journal |
Volume | Issue | ISSN |
130 | 2 | Discrete Applied Mathematics |
Citations | PageRank | References |
30 | 1.40 | 23 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Renato Bruni | 1 | 127 | 15.79 |