The anti-subsumptive enforcement of a clause δ in a set of clauses Δ consists in extracting one cardinality-maximal satisfiable sub- set Δ � 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, con- tain δ and are satisfiable with ¬δj where δj is some strict sub-clause of δ. On the contrary, we propose a method that avoids the computa- tion of this possibly exponential number of subsets of clauses. Interest- ingly, 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 pref- erence 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.
['Éric Grégoire', 'Jean-Marie Lagniez']
On Anti-subsumptive Knowledge Enforcement