Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae

In several applicative fields, the generic system or structure to be designed can be encoded as a CNF formula, which should have a well-defined satisfiability property (either to be satisfiable or to be unsatisfiable). Within a complete solution framework, we develop an heuristic procedure which is able, for unsatisfiable instances, to locate a set of clauses causing unsatisfiability. That corresponds to the part of the system that we respectively need to re-design or to keep when we respectively want a satisfiable or unsatisfiable formula. Such procedure can guarantee to find an unsatisfiable subformula, and is aimed to find an approximation of a minimum unsatisfiable subformula. Successful results on both real life data collecting problems and Dimacs problems are presented.