Finding out that a SAT problem instance F is unsatisfiable is not enough for applications, where good reasons are needed for explaining the inconsistency (so that for example the inconsistency may be repaired). Previous attempts of finding such good reasons focused on finding some minimally unsatisfiable sub-clause-set F' of F, which in general suffers from the non-uniqueness of F' (and thus it will only find some reason, albeit there might be others). In our work, we develop a fuller approach, enabling a more fine-grained analysis of necessity and redundancy of clauses, supported by meaningful semantical and proof-theoretical characterisations. We combine known techniques for searching and enumerating minimally unsatisfiable subclause-sets with (full) autarky search. To illustrate our techniques, we give a detailed analysis of well-known industrial problem instances. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Kullmann, O., Lynce, I., & Marques-Silva, J. (2006). Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the Lean Kernel. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4121 LNCS, pp. 22–35). Springer Verlag. https://doi.org/10.1007/11814948_4
Mendeley helps you to discover research relevant for your work.