On Anti-Subsumptive Knowledge Enforcement

Information

The anti-subsumptive enforcement of a clause δ in a set of clauses Δ consists in extracting one cardinality-maximal satisfiable subset Δ' of Δ∪{δ} that contains δ but that does not strictly subsume δ. 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.

This web page contains:

the runtime code and scripts of our approaches are available under Linux OS (runtime code and scripts)

a set of benchmarks (benchmarks )

a set of queries used for the presented experiments(queries )
a table synthesizing the empirical results (full table)

Here is how to compute one anti-subsumptive enforcement
Let BENCHMARK be a CNF instance, which must conform to the standard DIMACS format.
Let QUERY a text file where is reported (on a same line) a set of literal representing a clause δ.

This following command lines compute w.r.t. a clause δ (given in the file QUERY) and a formula Δ (given in the file BENCHMARK) one anti-subsumptive enforcement of δ in Δ

This combination executes naive approach: $ ./transformedApproach BENCHMARK QUERY -naive > TMP_FILE_NAIVE
$ ./executeNaive.sh TMP_FILE_NAIVE

Remark: The set clauses that has to removed to ensure the anti-subsumptive, is a hitting set on all the set of MCSes return by the procedure executeNaive.sh.

This combination executes the transformational appraoch: $ ./transformedApproach BENCHMARK QUERY > TMP_FILE_TRANSFORMED
$ ./executeMin.sh TMP_FILE_TRANSFORMED

Remark: The set clauses that has to removed to ensure the anti-subsumptive, is compute with respect to the model returns by the procedure executeMin.sh. More precisely, the problem becomes anti-subsumptive free when all the clause falsified by this one are removed.