Jean-Marie Lagniez (Université d’Artois)

The anti-subsumptive enforcement of a clause δ in a set of clauses ∆ consists in extracting one cardinality-maximal satisfiable subset ∆0 of ∆ ∪ {δ} that contains δ but that does not strictly subsume δ. In this paper, the computational issues of this problem are investigated in the Boolean framework. Especially, the minimal change policy that requires a minimal number of clauses to be dropped from ∆ can lead to an exponential computational blow-up. Indeed, a direct and natural approach to anti-subsumptive enforcement requires the computation of all inclusion-maximal subsets of ∆ ∪ {δ} that, at the same time, contain δ and are satisfiable with ¬δj where δj is some strict sub-clause of δ. On the contrary, we propose a method that avoids the computation of this possibly exponential number of subsets of clauses. Interestingly, it requires only one single call to a Partial-Max-SAT procedure and appears tractable in many realistic situations, even for very large ∆. Moreover, the approach is easily extended to take into account a preference pre-ordering between formulas and lay the foundations for the practical enumeration of all optimal solutions to the problem of making δ subsumption-free in ∆ under a minimal change policy.