On Anti-subsumptive Knowledge Enforcement

Abstract

The anti-subsumptive enforcement of a clause $\delta$ in a set of clauses $\varDelta$ consists in extracting one cardinality-maximal satisfiable subset $\varDelta '$ of $\varDelta \cup \{\delta \}$ that contains $\delta$ but that does not strictly subsume $\delta$. 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 $\varDelta$ 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 $\varDelta \cup \{\delta \}$ that, at the same time, contain $\delta$ and are satisfiable with $\lnot \delta _j$ where $\delta _j$ is some strict sub-clause of $\delta$. 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 $\varDelta$. 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 $\delta$ subsumption-free in $\varDelta$ under a minimal change policy.