Lean clause-sets: generalizations of minimally unsatisfiable clause-sets Original Research Article

We study the problem of (efficiently) deleting such clauses from conjunctive normal forms (clause-sets) which cannot contribute to any proof of unsatisfiability. For that purpose we introduce the notion of an autarky system A, which detects deletion of superfluous clauses from a clause-set F and yields a canonical normal form NA(F)⊆F. Clause-sets where no clauses can be deleted are called A-lean, a natural weakening of minimally unsatisfiable clause-sets opening the possibility for combinatorial approaches and including also satisfiable instances. Three special examples for autarky systems are considered: general autarkies, linear autarkies (based on linear programming) and matching autarkies (based on matching theory). We give new characterizations of (“absolutely”) lean clause-sets in terms of qualitative matrix analysis, while matching lean clause-sets are characterized in terms of deficiency (the difference between the number of clauses and the number of variables), by having a cyclic associated transversal matroid, and also in terms of fully indecomposable matrices. Finally we discuss how to obtain polynomial time satisfiability decision for clause-sets with bounded deficiency, and we make a few steps towards a general theory of autarky systems.