Propositional SAT solvers have been a popular way of computing justifications for ontological entailmentminimal subsets of axioms of the ontologies that entail a given conclusion. Most SAT encodings proposed for Description Logics (DLs), translate the inferences obtained by a consequence-based procedure to propositional Horn clauses, using which entailments from subsets of axioms can be efectively checked, and use modified SAT solvers to systematically search over these subsets. To avoid repeated discovery of subsets with already checked entailment, the modified SAT solvers add special blocking clauses that prevent generating truth assignments corresponding to these subsets, the number of which can be exponential, even if the number of justifications is small. In this paper, we propose alternative SAT encodings that avoid generation of unnecessary blocking clauses. Unlike the previous methods, the inferences are used not only for checking entailment from subsets of axioms, but also, as a part of the encoding, to ensure that the SAT solver generates truth assignments corresponding only to justifications.
Most Description Logic Reasoners, such as CEL [
One usually distinguishes between black-box and glass-box axiom pinpointing procedures.
Black-box procedures use only the yes/no answers provided by the reasoner, whereas
glassbox procedures also use other information, such as the set of inferences applied during the
entailment test. The set of inferences can be generated using consequence-based procedures
[
We assume the standard syntax and semantics of Description Logics (DLs) such as ℒ (see,
e.g., [
Example 1. Consider the ontology = { ⊑ , ⊑ , ⊑ , ⊓ ⊑ ⊥} and = ⊑ ⊓ . The entailment |= has 2 justifications: 1 = { ⊑ , ⊑ , ⊑ } and 2 = { ⊑ , ⊑ , ⊓ ⊑ ⊥}, and 3 repairs: 1 = { ⊑ }, 2 = { ⊑ }, and 3 = { ⊑ , ⊓ ⊑ ⊥}.
An inference is an expression inf of the form ⟨ 1, . . . , ⊢ ⟩ where 1, . . . , is a (possibly empty) sequence of axioms called the premises of inf, and is an axiom called the conclusion of inf. An inference ⟨ 1, . . . , ⊢ ⟩ is sound if { 1, . . . , } |= .
Let I be a set of inferences. An I-derivation from is a sequence of inferences = ⟨inf1, . . . , inf⟩ from I such that for every with 1 ≤ ≤ , and each premise of inf that is not in , there exists < such that is the conclusion of inf . An axiom is derivable from using I (notation: ⊢I ) if either ∈ or there exists an I-derivation = ⟨inf1, . . . , inf⟩ from such that is the conclusion of inf. A set of inferences I is complete for the entailment |= if |= implies ⊢I for every subset ⊆ . Example 2 (Example 1 continued). Consider a set I consisting of the following inferences: inf1: ⟨ ⊑ , ⊑ ⊢ ⊑ ⟩, inf2: ⟨ ⊑ , ⊑ ⊢ ⊑ ⊓ ⟩, inf3: ⟨ ⊑ , ⊑ ⊢ ⊑ ⊓ ⟩, inf4: ⟨ ⊑ ⊓ , ⊓ ⊑ ⊥ ⊢ ⊑ ⊥⟩, inf5: ⟨ ⊢ ⊥ ⊑ ⊓ ⟩, inf6: ⟨ ⊑ ⊥, ⊥ ⊑ ⊓ ⊢ ⊑ ⊓ ⟩.
Inference inf5 has no premises; all other inferences have 2 premises. Clearly, all inferences are sound. For axiom , and justifications 1 and 2 from Example 1, we have 1 ⊢I and 2 ⊢I due to the derivation 1 = ⟨inf1, inf2⟩ and 2 = ⟨inf1, inf3, inf4, inf5, inf6⟩ respectively. Therefore, I is complete for the entailment |= .
Note that if ̸|= then the entailment |= has no justification, has a single repair = ∅ and any set of inferences I is complete for |= .
In this section, we describe the MARCO algorithm for computing justifications and repairs [
Given an ontology and an axiom the algorithm computes the set of all justifications and minimal repairs for the entailment |= (which may or may not hold). The basic of the ontology such that |= , namely all ⊆ such that ⊆ . Similarly, each found repair ∈ determines subsets ⊆ such that ̸|= , namely those ⊆ such that ∩ = ∅. The SAT solver is used to discover the remaining subsets ⊆ , namely those ⊆ such that (1) ̸⊆
for every ∈ and (2) ∩ ̸= ∅ for every ∈ . As we will see, using each such subset either a new justification or a new minimal repair can be found.
To find a subset ⊆
for which the entailment |= is not yet known, Conditions (1) and (2) are encoded using propositional formulas. Specifically, each axiom ∈ is assigned to a distinguished propositional variable . Then each propositional assignment ℐ of these variables describes a subset (ℐ) = {
∈ | ℐ = 1}. The goal, therefore, is to construct a . This clause ensures that if ℐ = 1 then ℐ = 0 for some formula such that for each model ℐ of the subset (ℐ) satisfies (1) and (2).
To encode Condition (1), for each ∈ we add a new blocking clause ⋁︀{¬ | ∈ , hence /∈ (ℐ), and so ∈ } to ⋁︀{ |
̸⊆
(ℐ). Similarly, to encode Condition (2), for each ∈ , we add a new blocking clause The construction of the resulting formula as well as of new justifications and repairs is ∈ }. This clause ensures that ∈ (ℐ) for some ∈ . Hence (ℐ) ∩ ̸= ∅. described by Algorithm 1. We start with the empty set of justifications and repairs , as well as a tautological formula whose models ℐ describe all subsets (ℐ) ⊆ we repeatedly search for models of this formula using a SAT solver (Lines 2–12). For each (Line 1). Then such model ℐ (Line 3), we extract the corresponding subset = (ℐ) (Line 4) and test the entailment |= , e.g., using a reasoner (Line 5). If the entailment holds, this means that there exists a minimal subset ⊆
such that |= , i.e., a justification. This subset is found using function Minimize( |= ) (Line 6) to be discussed next. Due to Condition (1), must be diferent from any justifications in
found so far. Hence, we add this justification to (Line 7) and add to the encoding of (1) for this justification (Line 8). If ̸|= , we can compute a maximal superset ′ ⊇
of such that ′ ̸|= , and, consequently, a repair = ∖ ′ (Line 10). Again, due to Condition (2), must be diferent from any repairs from found so far.
Hence, we add to (Line 11) and add its encoding to (Line 12).
Minimizing entailments and maximizing non-entailments are preformed using two functions Minimize( |= ) and Maximize( ̸|= ) shown in Algorithm 1. For minimizing |= , we repeatedly remove from axioms
∈ unless this breaks the entailment. For maximizing |= , we repeatedly add remaining axioms ∈ ∖ unless this causes the entailment. Note that the results depend on the order in which the axioms are iterated, however, correctness of Algorithm 1 does not depend on the choice of minimal subsets or maximal supersets of .
Algorithm 1: Computing all justifications and minimal repairs using a SAT solver SAT-Pinpointing(, ): input : ontology and axiom output : the set of all justifications and of all minimal repairs for |= 5 6 7 8 9 10 11 12 1 ← ∅ , ← ∅ , ← ⊤ ; 2 while {ℐ | ℐ = 1} ̸= ∅ do 3 ℐ ← ℐ : ℐ = 1; 4 ← { ∈ | ℐ = 1}; if |= then ← Minimize( |= ); ← ∪ {}; ← ∧ ⋁︀{¬ | ∈ }; else ← ∖ Maximize( ̸|= ); ← ∪ {}; ← ∧ ⋁︀{ | ∈ }; 13 return , ;
Minimize( |= ): 14 for ∈ do 15 if ∖ { } |= then 16 ← ∖ { }; 17 return ;
Maximize( ̸|= ): 18 for ∈ ∖ do 19 if ∪ { } ̸|= then 20 ← ∪ { }; 21 return ; Example 3. Let us see how Algorithm 1 computes justifications 1, 2 and repairs 1, 2, 3 for the entailment |= in Example 1. We start by assigning propositional variables to axioms in as follows: ⊑ ⇝ 1, ⊑ ⇝ 2, ⊑ ⇝ 3, ⊓ ⊑ ⊥ ⇝ 4. Assume that each iteration of the while loop (Lines 2–12) returns a model shown in the first column of the table: ℐ 1 min( ) |= /
max( ) ̸|= ∅ ∪ { ⊑ , ⊑ } ̸|= { ⊑ } ∪ { ⊑ , ⊓ ⊑ ⊥} ̸|= { ⊑ , ⊑ } ∪ { ⊓ ⊑ ⊥} ̸|=
{ ⊑ , ⊑ , ⊑ } ∖ ∅ |= { ⊑ , ⊑ , ⊓ ⊑ ⊥} ∖ ∅ |= just/rep The second column shows the resulting set and its minimization (if |= ) or maximization (if ̸|= ). For example, the model in the first row corresponds to = ∅ ̸|= , which is maximized by adding axioms ⊑ and ⊑ . The third column shows the corresponding justification or repair from Example 1. The fourth column shows the clause resulting by encoding Conditions (1) and (2) for the found justification or repair. Each next propositional assignment in the first column must be a model of all previous clauses. After adding the 5 clauses in the table, the formula becomes unsatisfiable and Algorithm 1 terminates returning the content of the third column.
An advantage of Algorithm 1 is that it can compute justifications as well as repairs. However, in applications when only the computation of justifications is of main interest, e.g., for ontology debugging, the additional overhead for computing repairs can be significant. Indeed, as next example shows, the number of repairs can be exponential in the number of justifications. Example 4. Consider the ontology = { ⊑ , ⊑ | 1 ≤ ≤ }. Clearly, each subset = { ⊑ , ⊑ } (1 ≤ ≤ ) is a justification for the entailment |= ⊑ , and each subset containing exactly one axiom from each (1 ≤ ≤ ) is a repair. To compute these repairs, Algorithm 1 performs 2 calls to the SAT solver, each resulting in a new blocking clause.
Note that any black-box procedure that computes all justifications must perform an
exponential number of entailment tests for the ontology in Example 4 because an entailment test
must be performed for the complement of every repair to rule out further justifications. As seen
from Example 4, Algorithm 1 is particularly problematic if many, mostly independent, subsets
of the ontology are responsible for the entailment. A similar example can be constructed when
there are exponentially-many justifications but only linearly-many repairs (see, e.g., Example 23
in [
Assume that we have a set of sound inferences I that is complete for the entailment |= . That is, ⊢I if |= for every ⊆ (see Section 2). To find a repair for |= , we need to find a subset ⊆ such that ⊬I , i.e., is not derivable from using the inferences in I. According to the definition of derivability, this means that (1) /∈ , and (2) for every inference ⟨ 1, . . . , ⊢ ⟩ ∈ I, some of the premises is not derivable as well. This simple observation is a basis of our new SAT encoding for computing repairs.
Let us assign to each axiom appearing in I (as a premise or a conclusion) a distinct propositional variable . Intuitively, each propositional interpretation ℐ describes axioms with ℐ = 1 that should not be derived from . We call these axioms broken (hence the variable name ). According to Condition (1) above, we should have /∈ for all broken , so we take = (ℐ) = { ∈ | ℐ = 0} to be all non-broken axioms in . According to Condition (2), if ⟨ 1, . . . , ⊢ ⟩ ∈ I and is broken then one of the premises must be broken as well (1 ≤ ≤ ). We can encode this condition using a clause ¬ ∨ 1 ∨ · · · ∨ . Let be the conjunction of all such clauses for inferences in I plus . Then for every model ℐ of , we have = (ℐ) ⊬I , which implies ̸|= since I is complete for |= . Hence we can extract a repair of |= by maximizing the non-entailment ̸|= just like in Algorithm 1.
Algorithm 2 describes the above encoding and computations. We start with the empty set of repairs and initialize the formula as conjunction of and clauses for inferences in I as described above (Line 1). So long is satisfiable (Lines 2–7), we take a model of (Line 3), extract the subset = (ℐ) of non-broken axioms in (Line 4) for which our encoding guarantees that ̸|= . Then we maximize this non-entailment and extract the resulting repair just like in Algorithm 1 (Line 5), add this repair to (Line 6), and add the corresponding blocking clause (Line 7) to to ensure that this repair is not found by subsequent models. Example 5. Let us see how Algorithm 2 computes the repairs 1, 2, and 3 for the entailment |= in Example 1 using the set of 6 (sound and complete) inferences I from Example 2. Given these parameters, the function InitRepairs(, I) creates a conjunction of the following clauses: Algorithm 2: Computing all repairs using a SAT solver
SAT-Repair(, , I): input : ontology , an axiom, I a set of sound inferences complete for |= output : the set of all repairs for |= 1 ← ∅ , ← InitRepairs(, I); 2 while {ℐ | ℐ = 1} ̸= ∅ do 3 ℐ ← ℐ : ℐ = 1; 4 ← { ∈ | ℐ = 0}; 5 ← ∖ Maximize( ̸|= ); 6 ← ∪ {}; 7 ← ∧ ⋁︀{¬ | ∈ }; 8 return ;
InitRepairs(, I): 9 ← ; 10 foreach ⟨ 1, . . . , ⊢ ⟩ ∈ I do 11 ← ∧ (¬ ∨ ⋁︀{ | 1 ≤ ≤ }) 12 return ; 1. ⊑⊓ 2. ¬⊑ ∨ ⊑ ∨ ⊑ 3. ¬⊑⊓ ∨ ⊑ ∨ ⊑ 4. ¬⊑⊓ ∨ ⊑ ∨ ⊑ 5. ¬⊑⊥ ∨ ⊑⊓ ∨ ⊓⊑⊥ 6. ¬⊥⊑⊓ 7. ¬⊑⊓ ∨ ⊑⊥ ∨ ⊥⊑⊓ We highlighted in bold the variables assigned to axioms in since propositional assignments of these variables determine the subsets and the resulting repairs. The table below shows examples of models of and the resulting repairs obtained at each iteration of Algorithm 2: ℐ = 1 ⊑⊓ ⊑ ⊑ ⊑⊥ ⊑⊓ ⊑⊓ ⊑ ⊑ ⊑⊥ ⊑⊓ ⊑⊓ ⊑ ⊑⊥ ⊓⊑⊥ repair 1 2 3 new clause ¬⊑ ¬⊑ ¬⊑ ∨ ¬⊓⊑⊥ The first column lists all variables corresponding to the broken axioms. For the set of the remaining axioms from , our encoding guarantees that ̸|= . In our example, the sets are already maximal, so their complements (Line 5) correspond to repairs shown in the second column. Each of these repairs produces a new clause shown in the last column, which is added as a conjunction to . The algorithm, therefore, produces overall 7 + 3 = 10 clauses.
The main advantage of Algorithm 2 over Algorithm 1 is that generation of subsets of ⊆ with |= is completely avoided. The initial formula obtained by InitRepairs(, I), which has a linear size in the number of inferences in I, has the same efect as (potentially exponentially-many in the size of ) blocking clauses for justifications added to in Algorithm 2. A disadvantage of Algorithm 2 is that the new SAT encoding now involves more propositional variables (due to new axioms appearing in inferences), which could increase the search space of the SAT solver. Also, if the set of inferences I is considerably larger than the size of , the new translation might not pay of, particularly, if the number of justifications is relatively small.
We now extend the ideas used in the encoding for repairs in Section 4, to compute all justifications without computing repairs. Our goal is to construct a formula whose models correspond to only subsets ⊆ such that |= , or, equivalently, ⊢I . Recall that is derivable by inferences in I from if (1) ∈ , or (2) there exists an inference ⟨ 1, . . . , |= ⟩ ∈ I such that all premises 1, . . . , of this inference are derivable. To handle Condition (1) as a special case of (2), we extend the set I by adding, for every axiom ∈ , an “asserted axiom” inference ⟨ ⊢ ⟩, which means that any axiom in can be derived from no premises.
To express Condition (2) using a propositional formula, to each axiom appearing in I, we assign a distinguished propositional variable expressing that appears in the derivation of . In addition, to every inference inf ∈ I we, likewise, assign a distinguished variable inf expressing that this inference has been applied in the derivation of . Then Condition (2) is expressed using two types of clauses: 1. ¬ ∨ inf1 ∨ · · · ∨ inf , where inf 1, . . . , inf are all inferences in I with conclusion , 2. ¬inf ∨ , where is a premise of inf .
Let be the conjunction of all clauses above for all axioms and inferences inf appearing in I plus the unit clause expressing that must be derived. Similarly to the encoding for repairs in Section 4, we define a subset ⊆ using a model ℐ of by = (ℐ) = { ∈ | ℐ = 1}. The main question: does our encoding guarantee that |= ? Example 6. Let us apply the described translation for the entailment |= from Example 1 and the set of inferences I from Example 2. First, we extend I with inferences deriving axioms in : inf 7: ⟨ ⊢ ⊑ ⟩, inf 8: ⟨ ⊢ ⊑ ⟩, inf 9: ⟨ ⊢ ⊑ ⟩, inf 10: ⟨ ⊢ ⊓ ⊑ ⊥⟩. Then our encoding produces a formula , which is the conjunction of the following 20 clauses: 1. ⊑⊓ 2. ¬⊑ ∨ inf1 3. ¬⊑⊓ ∨ inf2 ∨ inf6 4. ¬⊑⊓ ∨ inf3 5. ¬⊑⊥ ∨ inf4 8. ¬⊑ ∨ inf8 9. ¬⊑ ∨ inf9 10. ¬⊓⊑⊥ ∨ inf10 11. ¬inf1 ∨ ⊑ 12. ¬inf1 ∨ ⊑ 13. ¬inf2 ∨ ⊑ 15. ¬inf3 ∨ ⊑ 16. ¬inf3 ∨ ⊑ 17. ¬inf4 ∨ ⊑⊓ 18. ¬inf4 ∨ ⊓⊑⊥ 19. ¬inf6 ∨ ⊑⊥ 6. ¬⊥⊑⊓ ∨ inf5 20. ¬inf6 ∨ ⊥⊑⊓ 7. ¬⊑ ∨ inf7 14. ¬inf2 ∨ ⊑ As before, bold variables correspond to axioms from . By checking satisfiability of , we may obtain the models shown in the first column of the following table: ⊑⊓ inf2 ⊑ ⊑ inf1
inf9 ⊑ ⊑ inf7 inf8 ⊑⊓ inf6 ⊑⊥ ⊥⊑⊓ inf4 inf5 ⊑⊓ ⊓⊑⊥ inf3 inf10 ⊑ ⊑ inf1 ⊑ justification
¬⊑ ∨ ¬⊑ ∨ ¬⊑ ¬⊑ ∨ ¬⊑ ∨ ¬⊓⊑⊥ The sets = (ℐ) extracted from these models consist of axioms corresponding to the bold variables and, as can be seen, correspond to justifications 1 and 2 from Example 1. If we now extend by adding the corresponding blocking clauses for these justifications shown in the third column, becomes unsatisfiable. Hence, no further sets and justifications can be produced. Example 7. Let us see how the new translation can avoid computing exponentially-many repairs for the entailment |= ⊑ from Example 4. Assume that we are given a set of inferences I = {inf = ⟨ ⊑ , ⊑ ⊢ ⊑ ⟩ | 1 ≤ ≤ }, which is, clearly, complete for this entailment. First, I is extended with inf ′ = ⟨ ⊢ ⊑ ⟩ and inf ′′ = ⟨ ⊢ ⊑ ⟩ (1 ≤ ≤ ). The translation creates Clauses 1 and 2 plus Clauses 3–6 for each with 1 ≤ ≤ : 1. ⊑ 2. ¬⊑ ∨ ⋁︀{inf | 1 ≤ ≤ } 3. ¬inf ∨ ⊑ 4. ¬inf ∨ ⊑ 5. ¬⊑ ∨ inf′ 6. ¬⊑ ∨ inf′′ After each call, due to Clauses 1–4, the SAT solver returns a model with iℐnf = ℐ⊑ = ℐ⊑ = 1 for some (1 ≤ ≤ ) from which the justification = { ⊑ , ⊑ } can be extracted. The added blocking clause ¬⊑ ∨ ¬⊑ ensures that inf ℐ = 0 in the subsequent models ℐ (due to Clauses 3 and 4). Hence, the procedure terminates after adding exactly additional clauses.
Examples 6 and 7 may suggest that |= always holds for subsets extracted from models of . However, this is true only if the set of inferences I is acyclic. An inference cycle (of length ) is a sequence of inferences [inf 1; inf 2; . . . ; inf ] such that the conclusion of inf is a premise of inf +1 (1 ≤ < ) and the conclusion of inf is a premise of inf 1. The cycle is elementary if all of its inferences have diferent conclusions. Clearly, each (non-elementary) cycle [inf 1; inf 2; . . . ; inf ] contains an elementary sub-cycle [inf ; . . . ; inf ] with 1 ≤ ≤ ≤ . A set of inferences I is cyclic if there is a cycle of inferences from I. Otherwise I is acyclic. Example 8. Let us extend the set of inferences I from Example 6 with two additional inferences: inf 11: ⟨ ⊑ ⊓ ⊢ ⊑ ⟩, inf 12: ⟨ ⊑ ⊓ ⊢ ⊑ ⟩.
The resulting set of inferences has 2 elementary cycles: 1 = [inf 3; inf 11] and 2 = [inf 3; inf 12]. Updating the encoding of the formula from Example 6 to the two additional inferences results in two modified clauses 2, 7, and two additional clauses 20, 21 shown below: 2. ¬⊑ ∨ inf1 ∨ inf 12 7. ¬⊑ ∨ inf7 ∨ inf 11 20. ¬inf11 ∨ ⊑⊓ 21. ¬inf12 ∨ ⊑⊓ The models of obtained in Example 6 are also models of the new clause set, however, there is also a new model shown below: ⊑⊓ inf2 ⊑ ⊑ inf12 inf9 ⊑⊓ inf3 ⊑ inf7 cycle 2
new clause ¬ inf 3 ∨¬ inf 12 Notice that = (ℐ) = { ⊑ , ⊑ } ̸|= = ⊑ ⊓ , so why did this happen in our translation? Note that the new model is similar to the first model in Example 6. The main diference is that to satisfy the (updated) clause 2, we now chose to make inf12 true instead of inf1 .
Algorithm 3: Computing all justifications using a SAT solver
SAT-Justification( , , I): input : ontology , an axiom, I a set of sound inferences complete for |= output : the set of all justifications for |= 8 9 10 11 12 13 14 15 This, intuitively, means that we chose to derive ⊑ by inference inf12 instead of inf1. To apply inf12, we need to derive ⊑ ⊓ first, so we make ⊑⊓ true. This axiom, in turn, can be derived using inf3 from ⊑ and ⊑ , so we make inf3 , ⊑ and ⊑ true. However, we now came back to ⊑ . This happened because of the inference cycle 2 = [inf3; inf12].
We can prevent generating models with cycle 2 by adding a blocking clause similar to blocking clauses for justifications shown in the last column. After adding this clause to the resulting formula becomes unsatisfiable, at which point we know that all justifications have been computed.
Algorithm 3 formalizes the overall procedure for computing justifications. We start with the empty set of justifications (Line 1), and extend the set of inferences I for axioms in (Line 2). Then we initialize our formula (Line 3) by adding the clauses for (Line 17), for each axiom in I (Line 19), and each inference in I (Line 21). For now, ignore Line 4 assuming that InitCycles(I) returns ⊤. Then, as usual, so long is satisfiable (Line 5), we take the model ℐ returned by the SAT solver (Line 6), determine the candidate subset of axioms = (ℐ) ⊆ (Line 7), and check the entailment |= (Line 8). If the entailment holds, we extract a new justification from as usual (Lines 8–11). If not, this can happen only due to a cyclic subset of inferences I∘ chosen by the model (Line 13), as we prove next. Note that ̸|= implies ∅ ⊬I∘ .
To find a cycle in I∘ (Line 14), we traverse these inferences backwards starting from the conclusion . To detect the cycle, we add conclusions to the set Visited, while collecting the expanded inferences in the list , both initially empty (Line 23). Our invariant is that ℐ = 1 but ∅ ⊬I∘ for every ∈ Visited, which clearly holds for the initial = . Having such , we first check that it was not already visited (Line 24) and add it to Visited (Line 25). Then we take any inference inf ∈ I∘ with conclusion (Line 26), which must exist due to the added clause for (Line 19) since ℐ = 1 and ℐ = 1. We prepend this inference to the list (Line 27). Finally, we choose the premise of inf such that ∅ ⊬I∘ . Note that such a premise exists since otherwise ∅ ⊢I∘ , which would contradict our invariant. Note also that ℐ = 1 for all premises of inf due to the initial translation for inf (Line 21). We reassign to the found premise (Line 28) and continue the while loop. Eventually we obtain ∈ Visited since the number of axioms is bounded, which means that a premise of the first inference in is a conclusion of some inference inf in . We traverse the list to find this inference inf, and return the prefix of ending with this inference (Line 29), which will be the elementary inference cycle we were looking for. After finding this cycle, we add the corresponding blocking clause to (Line 11), which makes sure that this cycle will not be a part of subsequent models of .
How many cycles could be encountered during a run of Algorithm 3? Since FindCycle(, I∘ ) produces only elementary cycles, the length of cycles is bounded by the number of inferences in I. Further, the set of inferences in each returned cycle is unique due to the added blocking clause in Line 11. Hence the number of cycles and such blocking clauses is at most exponential in the size of I. It may seem that Algorithm 3 sufers from the same problem as Algorithm 1: instead of enumerating possibly exponentially-many repairs we may need to enumerate possibly exponentially-many cycles in order to compute all justifications. As we show next, it is possible to extend the initial formula of the encoding to prevent cyclic models completely.
Let I be a set of inferences. Consider the binary relation on axioms appearing in I defined by the set of pairs = (I) = {⟨ , ⟩ | ⟨ 1, . . . , ⊢ ⟩ ∈ I, 1 ≤ ≤ }. It is easy to see that I is cyclic if the transitive closure + of contains a reflexive pair ⟨, ⟩ for some axiom . ⊑ ⇝ ⊑ ⇝ ⊑ ⇝ ⊓ ⇝ ⊑ ⇝ ⊑ ⊓ ⇝ Example 9. Let I be the set of (cyclic) inferences from Example 8. For conciseness, we number all axioms appearing in I and use these numbers instead of the original axioms: 1 4 7 2 5 8 3 6 9 ⊑ ⊥ ⇝ ⊥ ⊑ ⊓ ⇝ ⊑ ⊓ ⇝
Then the set of inferences I defines the set = (I) of pairs of numbers corresponding to these axioms shown in the right picture by solid lines. As can be seen, nodes 1 and 6 as well as nodes 5 and 6 form cycles in this graph. The transitive closure + of extends this relation with the additional pairs shown by the dashed red lines. As can be seen, the extended graph contains 3 reflexive pairs: ⟨1, 1⟩, ⟨5, 5⟩, and ⟨6, 6⟩. 6 4 8 2 9 1 7 3 5
Let = (I) be the set of pairs induced by inferences from I. For each pair ⟨, ⟩ ∈ + we introduce a distinguished propositional variable , ⟩. Consider the following clauses: ⟨ 2. ¬⟨, ⟩ ∨ ¬⟨, ⟩ ∨ , ⟩ for every ⟨,
⟨ 3. ¬⟨, ⟩ for every ⟨, ⟩ ∈ +. 1. ¬inf ∨ ⟨ , ⟩ for every inf = ⟨ 1, . . . , ⊢ ⟩ ∈ I and 1 ≤ ≤ , ⟩ ∈ + and ⟨, ⟩ ∈ , Intuitively, clauses of Form 1 express that if an inference ⟨ 1, . . . , ⊢ ⟩ ∈ I is selected by the model, then all pairs ⟨ , ⟩ ∈ (1 ≤ ≤ ) must be selected by this model as well. Clauses of Form 2 express that the pairs selected by the model are transitively closed. Finally, clauses of Form 3 express that no reflexive pair from + can be selected by the model.
Suppose that the function InitCycles(I) produces the conjunction of all clauses of Forms 1-3 as described above. By using this function in Line 4 of Algorithm 3, we make sure that for every model ℐ of , the set of inferences I(ℐ) = {inf ∈ I | iℐnf = 1} is acyclic. Hence the else-part of the algorithm (Lines 12–15) never applies, and each model found by the SAT solver corresponds to a new justification. Clearly, the number of clauses of Form 1 is linear in the size of I. Since the number of axioms appearing in I and the number of pairs ⟨, ⟩ ∈ are linear in the size of I, the number of clauses of Form 2 is quadratic in the size of I and the number of clauses of Form 3 is linear. Thus, the maximal number of clauses generated by Algorithm 3 can be reduced from exponential to quadratic.
In this paper, we have described new SAT-based procedures for computing repairs and justiifcations from a set of inferences. Unlike the previous methods, we use inferences not only for entailment checks, but also to avoid generating unnecessary models. While for computing repairs our encoding requires a linear number of additional clauses, computing justifications may require a quadratic number of clauses in order to block cyclic models.
There appears to be a strong connection between our encodings and reductions of Answer
Set Programming (ASP) to SAT [
For some ontologies, such as OpenGALEN [37], for which the generated proofs can be very
large and cyclic [
By combining encoding for repairs and justifications, it is also possible to obtain a procedure for computing the unions of justifications (= the unions of repairs), which were recently of some interest [38, 39, 40]. This procedure can compute the unions using at most calls of the SAT solver, where is the size of the resulting union. This is optimal since the membership problem for unions of justifications is already NP-Complete (see Theorem 7 in [ 41]). Our preliminary empirical experiments on some selected dificult examples have been very promising. Unfortunately, we have no space left in this paper to discuss these results in detail. [34] T. Janhunen, Some (in)translatability results for normal logic programs and propositional theories, J. Appl. Non Class. Logics 16 (2006) 35–86. [35] K. L. Clark, Negation as failure, in: H. Gallaire, J. Minker (Eds.), Logic and Data Bases, Symposium on Logic and Data Bases, Centre d’études et de recherches de Toulouse, France, 1977, Advances in Data Base Theory, Plemum Press, New York, 1977, pp. 293–322. URL: https: //doi.org/10.1007/978-1-4684-3384-5_11. doi:10.1007/978-1-4684-3384-5\_11. [36] F. Fages, Consistency of Clark’s completion and existence of stable models, Methods Log.
Comput. Sci. 1 (1994) 51–60. [37] A. L. Rector, J. Rogers, P. E. Zanstra, E. J. van der Haring, OpenGALEN: Open source medical terminology and tools, in: AMIA, AMIA, 2003. [38] M. Janota, J. Marques-Silva, cmmus: A tool for circumscription-based MUS membership testing, in: LPNMR, volume 6645 of Lecture Notes in Computer Science, Springer, 2011, pp. 266–271. [39] C. Mencía, O. Kullmann, A. Ignatiev, J. Marques-Silva, On computing the union of MUSes, in: SAT, volume 11628 of Lecture Notes in Computer Science, Springer, 2019, pp. 211–221. [40] J. Chen, Y. Ma, R. Peñaloza, H. Yang, Union and intersection of all justifications, in: ESWC, volume 13261 of Lecture Notes in Computer Science, Springer, 2022, pp. 56–73. [41] R. Peñaloza, B. Sertkaya, Understanding the complexity of axiom pinpointing in lightweight description logics, Artif. Intell. 250 (2017) 80–104.