Designing reliable logic programs becomes especially challenging when constraints are involved, i.e., rules that must never be violated, no matter the input. Therefore, constraints may induce conflicts with other rules that derive the literals in their bodies, causing constraint-induced inconsistencies (CI-inconsistencies). In this paper, we introduce a new consistency notion for answer set programming: robust CI-consistency, which ensures that a program's constraints are respected under all admissible sets of facts. Our focus lies on positive constraints, a natural and intuitive class that avoids default negation and expresses hard requirements on the program's output. To support knowledge engineers in early stages of modelling, we present a method that allows the expert to define general constraints and selectively refines only the rules that could lead to violations. This is achieved by extending the idea of -extensions, originally developed for handling contradictions caused by strong negation. By systematically identifying problematic rule combinations and adjusting them just enough to prevent conflicts caused by future instance data, our approach yields encodings that are correct by design in any case-without deleting rules or depending on specific data. This framework helps bridge the gap between early, intuitive modelling and robust, instance-independent correctness.
Answer Set Programming (ASP) is a declarative paradigm for knowledge representation and reasoning, well-suited to solving combinatorial problems. In practice, an ASP program is usually divided into two components: the encoding, which defines the general rules of the problem, and the instance, which provides concrete input data as facts. This separation enables a single encoding to be applied to multiple instances, akin to executing software with diferent input data.
However, in high-stakes applications such as medical decision support systems, it is critical to ensure that an encoding behaves reliably across all admissible instances (e.g., patient data). Constraints can play a vital role in such contexts–for example, by preventing the recommendation of therapies or drugs with known adverse interactions. Domain experts may define hard constraints to enforce compliance with clinical guidelines or to block recommendations involving harmful combinations. While such constraints are essential for ensuring correctness, they can inadvertently introduce inconsistencies if the encoding fails to anticipate rare or exceptional cases. This, in turn, may cause the program to become inconsistent, rendering the encoding unusable for certain instances.
Prior works [
In this work, we extend this approach to constraint-induced inconsistencies (CI-inconsistencies). We enable knowledge engineers to define problem encodings in a more general way, without needing to account for every exception or rare case individually in the first place. The system will check if any 23rd International Workshop on Nonmonotonic Reasoning, November 11–13, 2025, Melbourne Australia * Corresponding author. $ andre.thevapalan@tu-dortmund.de (A. Thevapalan); gabriele.kern-isberner@cs.tu-dortmund.de (G. Kern-Isberner) 0000-0001-5679-6931 (A. Thevapalan); https://orcid.org/0000-0001-8689-5391 (G. Kern-Isberner)
© 2025 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). admissible instances lead to the activation of constraints. If such instances arise, the system signals the issue, allowing the engineer to fine-tune the relevant rules in the encoding. This ability to dynamically refine encodings while maintaining the integrity of the constraints makes the approach particularly well-suited for complex, real-world scenarios, ensuring robust, consistent, and tailored solutions. Our approach motivates the usage of constraints by emphasising their critical role in ensuring that the program behaves as intended. Instead of manually handling each potential inconsistency, engineers can specify constraints that act as strict guards, preventing undesired answer sets. This allows them to focus on creating flexible, reusable encodings, while leaving the responsibility of ensuring correctness to the constraints, which guide the system in preventing unintended behaviours.
The remainder of this paper is structured as follows. Section 2 introduces the necessary preliminaries
on answer set programming to establish the formal background. In Section 3, we review related
work and summarise the existing approach in [
In this paper, we examine the propositional fragment of non-disjunctive extended logic programs
(ELPs) [
⋆ is either a literal or its default negation ∼ . We also extend ∼ to sets: for a set of literals, ∼ = {∼ | ∈ } . We will use ∼ as a unary junctor in order to describe the default complement of an extended literal: for an extended literal ⋆, the default-complementary literal ∼ ⋆ is defined as ∼ if ⋆ = , and otherwise.
A set of extended literals is said to be inconsistent if it contains strongly or default-complementary literals. Two extended literals ⋆ and ⋆ are referred to as mutually exclusive if they are strongly complementary or default-complementary.
underlying set of atoms in a set of extended literals is denoted by () = {(⋆) | ⋆ ∈ }.
A rule is of the form: () ← +(), ∼ − ().
(1) where (), called the head of , is either a singleton set {} for some literal , or the empty set ∅. The sets +() and − (), called the positive and negative body of , respectively, are (possibly empty) sets of literals. The body of is defined as () = +() ∪ ∼ − ().
A rule is called a fact if () = ∅ , and a constraint if () = ∅. A constraint is said to be positive if − () = ∅; note that positive constraints may still contain strong negation.
An extended logic program (ELP) is a set of rules of the form (1). In the remainder of this paper, we assume that any ELP is over the set of atoms occurring in .
Given an ELP , we distinguish the following components: the set Φ of facts, referred to as the problem instance of ; the set Ψ of constraints; and set Π of all remaining rules, referred to as the problem encoding of . To each problem encoding Π , we associate its set of external atoms, denoted by ℰ (Π) ⊆ , defined as the set of atoms that occur in Π but not in the head of any rule in Π.
We illustrate the components of an ELP using the following running example.
Example 1. Consider a simplified medical decision-support system that recommends treatments based on suspected diagnoses, which we use as a running example.
1: leuk ← anem, ∼abnSk .
2: mela ← lesn, ∼swLn. 3: chem ← leuk , imsp. 5: ← chem, imtx .
4: imtx ← mela, ∼aid .
This program models the diagnosis and treatment process for leukaemia (leuk ) and melanoma (mela), two cancers that typically do not occur together except in rare cases. If a patient has anaemia (anem) and no visible skin abnormalities (abnSk ), leukaemia is suspected. If the patient has a lesion (lesn) but no swollen lymph nodes (swLn), melanoma is diagnosed. If leukaemia is confirmed and the patient is not immunosuppressed (imsp), chemotherapy (chem) is prescribed. If melanoma is diagnosed and there is no autoimmune disorder (aid ), immunotherapy (imtx ) is recommended.
The integrity constraint in 5 ensures that both therapies are not prescribed together. This is because chemotherapy and immunotherapy target diferent mechanisms and may have adverse interactions if used in combination, making their joint application inappropriate for the patient’s safety.
The rules 1–4 form the problem encoding Π 1, while Ψ 1 = {5} defines the constraint set, preventing the simultaneous prescription of both therapies. Possible problem instances Φ 1 are facts corresponding to subsets of the external atoms ℰ (Π 1) = {anem, abnSk , lesn, swLn, imsp, aid }.
We now move on to the semantics of ELPs.
Let be a set of literals. A literal is said to be true in if ∈ , false in if ∈ , and unknown otherwise. A rule is applicable under if +() ⊆ and − () ∩ = ∅. The set satisfies the body () of a rule if is applicable under . The set satisfies a rule if and only if () ∩ ̸= ∅ whenever satisfies (). A set of literals supports a rule if is applicable and satisfied under . We say is unsatisfiable if there exists no consistent set of literals s.t. is applicable under .
Note: If is a constraint, then satisfies if does not satisfy (). Conversely, if satisfies the body of a constraint, we say that violates .
In general, an answer set of an ELP is determined by its reduct. The reduct of a program relative to a set of literals is defined as: = {() ←
+(). | ∈ , − () ∩ = ∅}.
Note that any reduct contains no default negation.
For programs without default negation, we define the closure Cl () of as the smallest subset
⊆ ℒ such that satisfies all rules in . Notably, similar to Horn logic programs, each ELP without
default negation has exactly one closure Cl (), which may, however, be inconsistent (cf. [
Let be an ELP over , and assume contains no default negation. The answer set of is defined as follows: (a) if Cl () is consistent, then Cl () is the unique answer set of ; (b) otherwise, the answer set of is defined to be ℒ , i.e., the complete set of literals over .
A set of literals is an answer set of an ELP if it is the answer set of the reduct [
Ψ 1 from Example 1, and the following problem instance Φ 2 = {anem.}. Then, 2 has the unique answer set 1 = {anem, leuk , chem}.
The authors in [
In [
The authors in [
The authors in [
On an implementation level, constraints are transformed in such a way that their constraint violation
results in an incoherent program, that is, a program without any answer sets due to cyclic dependencies.
In [
In contrast to these methods, which rely on constraint deletion, instance-specific grounding, or syntactic meta-rewriting, our framework operates directly on the problem encoding. It treats constraints as semantic sources of inconsistencies with derivable literals and resolves these inconsistencies via constraint-guarding -extensions, rather than through removal or instance-dependent diagnosis.
In [
Definition 1 (SC-Consistency and SC-Inconsistency). Let be an ELP. The program is said to be SC-inconsistent (strong complementarity inconsistent) if every set ⊆ ℒ satisfying (2) is inconsistent, i.e., contains a pair of strongly complementary literals and . Otherwise, is said to be SC-consistent. Example 3. Suppose the following program 3: 1: ← . 4: ← ∼.
2: ← .
5: .
3: ← ∼.
6: .
Only = {, , , , } satisfies condition (2). Hence, 3 is SC-inconsistent.
Intuitively, a program is SC-inconsistent if strongly complementary literals can be derived from ; otherwise, it is SC-consistent.
Note that the term SC-inconsistency is not used in the original papers by Thevapalan and KernIsberner; we introduce it here to clearly distinguish this particular form of inconsistency from others.
A problem encoding Π is said to be robustly SC-consistent if it remains SC-consistent when combined
with any admissible problem instance Φ , that is, any instance constructed using atoms in ℰ (Π) . In [
1; cf. [
The rules in are referred to as conflicting and Γ
() denotes the set of all conflicts in involving .
We illustrate the notion of conflicts with the following example.
Example 4. In Example 3, 3 contains the conflicts 1 = {1, 2}, 2 = {1, 3}, and 3 = {1, 4}.
We now briefly recall the fundamental conflict-resolution techniques introduced in [
We begin by recalling the characterisation of conflicts as provided in [
conditions hold: (CP1) (), (′) are strongly complementary; (CP2) +(1) ∩ − (2) = ∅ for 1, 2 ∈ {, ′}, 1 ̸= 2; (CP3) +() ∪ +(′) is consistent.
Conditions (CP2) and (CP3) imply that such conflicts can be resolved by modifying the rule bodies to
prevent their simultaneous applicability under any consistent set of literals. This motivates the notion
of conflict-preventing literals:
Definition 3 (Conflict-Preventing Literals; cf. [
Conflict-preventing literals make it possible to resolve conflicts, as formalised in the following
proposition:
Proposition 1 ([
Hence, the addition of conflict-preventing literals yields rules that are no longer simultaneously applicable. This leads to the notion of conflict-resolving -extensions.
Definition 4 ( -Extension; cf. [
The corresponding -extended rule w.r.t. () is:
⋆: () ← (), ().
(3)
1In the original literature, the term conflict is used. We adopt the prefix SC- to distinguish this notion from conflicts that are
induced by constraints.
2Note that this condition is an additional requirement not present in the original definition of -extensions [
To resolve all conflicts involving , suitable -extensions can be applied.
A -extension () is conflict-resolving if for every conflict ⋆ ∈ () and ⋆
∈ (′) such that ⋆ and ⋆ are conflict-preventing.
Definition 5 (Conflict-Resolving
-Extension; cf. [
{, ′} ∈ Γ (), there exist extended literals
In [
We continue Example 3 to illustrate the concept.
Example 5 (Example 3 contd.). For the rule 1 in Π 3, two conflict-resolving -extensions exist: 1(1) = {∼, , },
2(1) = {, , }.
-extensions are informative, as they aim to preserve the original knowledge as far as possible, rather
than simply disabling conflicting rules entirely or enforcing rigid prioritisation schemes. Instead,
extensions extend existing rule bodies in a minimal way, using only atoms directly related to the specific
conflict. As argued in [
Example 6 ([
p_algy ← pos_test .
eat _p ← p_algy .
This program treats an individual as non-allergic if they did not experience an allergic reaction, and explicitly allergic if they tested positive. Those not allergic can eat peanuts.
According to [
Following the approach in [
p_algy ← pos_test .
eat _p ← p_algy . Φ ∪ Π
′6′ yields the intended answer set {pos_test , p_algy }.
The notion of conflicts is closely linked to SC-inconsistency. Specifically, whenever a program
SC-inconsistent, then for any set of literals satisfying (2), there exists a conflict in such that both
bodies of are simultaneously satisfied by . Consequently, the absence of such conflicts guarantees
that strongly complemementary literals cannot be derived.
is
Proposition 2 (cf. [
In summary, the framework proposed in [
In the following, we make some assumptions on the programs to be considered that help us focus on
repairing CI-inconsistencies. First, we assume that programs are not SC-inconsistent (Definition 1), as
such inconsistencies have already been addressed in [
While syntactically simple, positive constraints are semantically strict: they are violated as soon as their body is satisfied, and, due to their monotonic nature, such violations persist. This makes them particularly brittle in dynamic, instance-driven settings, where they often constitute a primary source of inconsistency.
At the same time, positive constraints are particularly well-suited for practical ASP development. They ofer a declarative and intuitively interpretable way to specify global properties of desired answer sets, and we demonstrate that they align naturally with established methods such as conflict resolution via -extensions.
By providing a mechanism to assess whether a constraint is violated under certain instances, our approach enables domain experts to fine-tune the conditions under which specific rules apply. In this way, rules can initially be specified in coarse form, without encoding every possible exception, and refined later as needed by considering concrete possible cases to ensure consistency w.r.t. constraints.
This promotes a modular and iterative modelling paradigm: positive constraints serve not only to enforce properties of answer sets, but also as diagnostic tools for identifying and resolving problematic interactions between the encoding and instance data.
We now adapt the notion of conflicts to the setting of positive constraints. The answer sets of an ELP are determined by constructing those of Π ∪ Φ and verifying that they satisfy all constraints in Ψ . While Φ ∪ Π generates candidate answer sets, the constraints in Ψ act as filters that eliminate those violating specific conditions. Notably, constraint satisfaction can be evaluated after the solving of answer sets for the unconstrained part of the program.
answer set of Π ∪ Φ that satisfies all constraints from Ψ .
Using these results, we can now define the notion of CI-(in)consistency:
encoding Π and the set of constraints Ψ . is CI-inconsistent (integrity constraint inconsistent) if there exists at least one answer set = Cl ((Φ ∪ Π )), but each such set violates at least one constraint in Ψ . Conversely, is called CI-consistent if there exists an answer set = Cl ((Π ∪ Φ )) that satisfies all constraints from Ψ .
CI-(in)consistency is determined based on Corollary 1: fixpoints of the program without constraints are computed first, and each resulting answer set is then checked for constraint violation.
Thus, each constraint ∈ Ψ acts as a safeguard that eliminates undesired answer sets from Φ ∪ Π . This mechanism allows the knowledge engineer to formulate general rules in Π , while relying on constraints to rule out unintended outcomes.
Example 7 (Example 1 contd.). Let Π 1 be the problem encoding and Ψ 1 the set of constraints as described in Example 1. Consider the problem instance Φ 7 = {anem., lesn.} The program 7 = Π 1 ∪ Φ 7 has the unique answer 7 = {anem, lesn, leuk , mela, chem, imtx }. However, when the constraint in Ψ 1 is included, the resulting program 7′ = Π 1 ∪ Φ 7 ∪ Ψ 1 has no answer sets because of constraint 5, which eliminates 7 as an answer set.
apy. While each treatment rule is valid in isolation, certain combinations of external atoms (e.g., facts asserting leuk and mela) may lead to both chem and imtx being derived, thereby activating the constraint and eliminating the answer set. From a clinical view, such constraints are critical safeguards against harmful treatment recommendations.
To ensure that a problem encoding remains consistent across diferent input data, we define admissible problem instances as those that do not directly violate any constraint in the encoding. For example, for an encoding with the constraint ‘← , ’, any problem instances containing both and are inadmissible. Specifically, while instance literals may appear in constraint bodies, each constraint must retain a suficient dependency on the encoding. That is, constraints should not be violated merely due to the presence of certain input facts, but should require the derivation of literals through the program’s rules.
a problem instance Φ is said to be admissible w.r.t. Ψ if for each constraint ∈ Ψ the following holds: () ∩ ⋃︀∈Φ () = ∅.
This ensures that each constraint requires all body literals must be derived through the encoding, thereby linking constraint violations to the behaviour of the program rather than the input.
Using the notion of admissible problem instances, we define robustly CI-consistent problem encodings: Definition 8 (Robust CI-Consistency). Let Π be a problem encoding and Ψ a set of (positive) constraints. The encoding Π is referred to as robustly CI-consistent if, for every admissible problem instance Φ , the combined program Π ∪ Φ ∪ Ψ is CI-consistent.
Remark: The notion of robust consistency is related to the concept of super-coherence [
In the remainder of this paper, we demonstrate how a problem encoding can be systematically
transformed to ensure robust CI-consistency across all admissible instances. Our approach builds
on and extends existing methods by addressing inconsistencies that arise through the interaction of
the encoding with integrity constraints, with a particular emphasis on constraint-induced violations.
This complements the work in [
In the following, a rule set refers to a set of at least two rules, such that every rule in the set has a non-empty head3. To support several definitions introduced later in this paper, we additionally introduce the notion of body-compatible and compatible rule sets.
Definition 9 ((Body-)Compatible Rule Sets). A rule set if there exists a set of literals such that ℛ is called body-compatible (resp., compatible) 3Singleton rule sets are excluded, as our approach explicitly examines the interactions between multiple rules. (1) is consistent, and (2) for every rule ∈ ℛ, satisfies () (resp., satisfies () ∪ ()).
Otherwise, we call ℛ body-incompatible (resp., incompatible).
Note that any compatible rule set is, in particular, body-compatible. (body-)compatible rule set ℛ is downward closed, i.e., every subset ℛ ⊆ ℛ ′ (body-)compatible.
Furthermore, we obtain the following characterisation:
Furthermore, any with |ℛ′| ≥ 2 is also
(BC1) For all rules , ′ ∈ ℛ the sets +() and − (′) are disjoint, i.e., +() ∩ − (′) = ∅. (BC2) The union of the positive bodies of the rules in ℛ is consistent, i.e., ⋃︀∈ℛ +() is consistent. (BC3) For all rules , ′ ∈ ℛ, no head literal appears as a negative body literal in ℛ, i.e., ()∩− (′) = ∅ Proof. Let ℛ ⊆ . (⇒) Assume that ℛ is compatible. Then, by Definition 9, there exists a consistent set such that supports ∈ ℛ. We now show that (BC1), (BC2), and (BC3) hold. • (BC1): Assume, for contradiction that there exist , ′ ∈ ℛ such that there exists a literal ∈ +() ∩ − (′). Since satisfies (), we have ∈ . However, for to satisfy (′), it must hold that ∈/ , leading to a contradiction. Hence, (BC1) holds. • (BC2): Let := ⋃︀∈ℛ +(). Suppose, for contradiction, that is inconsistent. Then there exists an atom such that both and ¬ occur in , implying that no consistent set can satisfy all +(), contradicting the assumption that ℛ is compatible. Hence, is consistent and (BC2) holds. • (BC3): Suppose, for contradiction, that there exist rules , ′ ∈ ℛ such that there exists a literal ∈ () ∩ − (′). Since satisfies (), the head literal must be in . But since ∈ − (′), satisfying (′) requires ∈/ , again yielding a contradiction. Therefore (BC3) holds. (⇐) Conversely, suppose a rule set ℛ ⊆ that satisfies (BC1), (BC2) , and (BC3). To show that ℛ is compatible, define the set := ⋃︀∈ℛ +() ∪ ⋃︀∈ℛ ().
Consistency of : This follows directly from (BC2), which ensures that the union of positive bodies is consistent, and from the assumption that is robustly SC-consistent.
Support of rules in ℛ: To show that satisfies all rules in ℛ, we must verify for each ∈ ℛ that (S1) +() ⊆ and (S2) − () ∩ = ∅. Condition (S1) holds by construction of , since includes all positive body literals. For condition (S2), fix ∈ ℛ. For any ′ ∈ ℛ, we know from (BC1) that +(′) ∩ − () = ∅, and (BC3) that (′) ∩ − () = ∅. Hence, since ⊆ ⋃︀′∈ℛ +(′) ∪ ⋃︀′∈ℛ (′), it follows that − () ∩ = ∅. Therefore, all rules in ℛ are supported under the consistent set , and thus ℛ is compatible.
The notion of (body-)compatibility is introduced to identify rule sets that may jointly violate a constraint, thereby serving as a basis for detecting potential constraint violations. This enables the application of constraint-guarding techniques–akin to the use of conflict-preventing literals–to strategically mitigate such interactions.
Example 8. Suppose the following problem encoding Π 8: 1: ← , ∼.
2: ← , ∼ℎ.
3: ← , ∼.
Rather than removing or modifying constraints, we examine the rules whose interactions lead to their violation. To this end, we introduce the notion of CI-conflicts: Definition 10 (Constraint-Induced Conflicts (CI-Conflicts)). Let Π be a problem encoding and a positive constraint over with at least two literals. A rule set ℛ ⊆ Π is called a constraint-induced conflict (CI-conflict) w.r.t. if (1) each literal in () appears as the head literal of exactly one rule in ℛ, and (2) ℛ is compatible. The rules in an CI-conflict w.r.t. are said to violate the positive constraint .
w.r.t. 5.
CI-conflicts explain how the body of a constraint might be satisfied. Their absence guarantees that no positive constraint is violated.
Theorem 3. Let Π be a problem encoding, and Ψ a set of positive constraints. If Π contains no CIconflicts w.r.t. any ∈ Ψ , then for any admissible problem instance Φ w.r.t. Π , we have (Π ∪ Φ) = (Π ∪ Φ ∪ Ψ).
Proof. Let := Π ∪ Φ , and let ′ := Π ∪ Φ ∪ Ψ . By Proposition 3, (′) = { ∈ () | satisfies all constraints in Ψ}. Assume that Π contains no CI-conflict w.r.t. any ∈ Ψ . We aim to show that under this assumption, every answer set ∈ () satisfies all constraints in Ψ.
Suppose, for contradiction, that there exists ∈ () violating some ∈ Ψ . Since is positive, () ⊆ . Hence, for each literal ∈ (), there exists a rule with () = {} such that is applicable under , i.e., was used to derive .
Moreover, since Φ is an admissible problem instance and contains no facts for deriving literals in the bodies of constraints, the derivation of literals in () relies solely on rules from Π and Φ . Consequently, there exists a set ℛ ⊆ Π such that for every ∈ (), some ∈ ℛ has () = {} and is supported under . The rules in ℛ are compatible, implying that ℛ constitutes a CI-conflict w.r.t. , contradicting our assumption.
Hence, every ∈ () satisfies all constraints ∈ Ψ, and thus () = ( ′).
As a direct consequence of Theorem 3 and Definition 10, we obtain the following characterisation: Corollary 2. Let Π be a problem encoding and Ψ a set of positive constraints such that Π contains no CI-conflicts w.r.t. any positive constraint ∈ Ψ . Then, Π is robustly CI-consistent, that is, for any admissible problem instance Φ, the combined program Π ∪ Φ ∪ Ψ is CI-consistent.
By modifying the rules in a CI-conflict ℛ such that their bodies cannot become satisfied, unintended constraint violations can be prevented.
To introduce the notion of constraint-guarding -extensions (CG -extensions), we now return to the running example: Example 10 (Example 1 contd.). Let Π 10 be derived from Π 1 by replacing rule 3 with 3′: chem ← leuk , imsp, ∼mela. Then, the program 10 = Π 10 ∪ {imsp, anem, lesn} ∪ {5} has the unique answer set {imsp, anem, lesn, leuk , mela, imtx }.
The modification of 3 ensures that chemotherapy is only recommended if melanoma is not suspected. From a medical perspective, this change reflects a prioritisation of melanoma treatment. When both cancers are present–a rare but critical scenario–immunotherapy takes precedence, as it is more sensitive to treatment timing and potential interaction. By adding ∼mela , the system avoids recommending chemotherapy in such cases, preserving clinical safety.
This anticipatory adjustment disables the application of 3 when conflicting statements arise due to (often rare, but) admissible problem instances, without compromising the intended logic of individual rules. This fine-tuning of the program helps the expert to avoid overlooking critical cases while still enabling the formalisation of their knowledge in generic (default) rules.
As a result, the program remains consistent across all admissible problem instances.
These observations lead us to the following definition.
Definition 11 (Constraint-guarding -Extension (CG -Extension)). Let Π be a problem encoding, Ψ a set of constraints, and ∈ Ψ a positive constraint. Let ℛ ⊆ Π be a CI-conflict w.r.t. . A -extension () ∈ ℛ is referred to as a constraint-guarding -extension (CG -extension) w.r.t. if there exist two extended literals ⋆ in () and ⋆ in some rule ′ ∈ ℛ such that ⋆, ⋆ are mutually exclusive. The extended literal ⋆ ∈ () is then referred to as a guard literal.
Lemma 1 (Condition for Existence of Constraint-Guarding -Extensions). Let be a rule in an ELP , and suppose there exists a CI-conflict ℛ w.r.t. some positive constraint such that ∈ ℛ. The exists a CG -extension () if there is a rule ′ ∈ ℛ and an extended literal ⋆ ∈ (′) ∖ () such that (⋆) ∈/ (()), and (⋆) ∈/ (()).
Proof. We prove the contrapositive: Suppose that for all ′ ∈ ℛ and all ⋆ ∈ (′) ∖ (), either (⋆) ∈/ (()), or (⋆) ∈/ (()). Then no CG -extension () exists.
Assume that for every ′ ∈ ℛ, every extended literal ⋆ ∈ (′) ∖ () satisfies (⋆) ∈ (()) ∪ (()). This implies there exists no literal in (′) ∖ () whose atom is disjoint from both the body and the head of .
Suppose we attempt to construct a CG -extension () . To do so, we must add a guard literal ∼ ⋆ (alternatively ⋆) to the body of , aiming to make body-incompatible with some ′ ∈ ℛ while leaving ′ unafected. This requires that ⋆ occurs in (′) but not in (), and (⋆) does not appear in () ∪ (), to ensure ∼ ⋆ is a valid guard and does not interfere with the existing semantics of ′. However, by our assumption, every candidate literal ⋆ ∈ (′) ∖ () fails this requirement as its atom is already present in . Hence, any attempt to use ∼ ⋆ as a guard literal either introduces redundancy, or creates self-blocking behaviour (if the atom occurs in ()), or results in no incompatibility with ′ at all. Consequently, no valid guard literal exists to distinguish from ′, and thus no constraint-guarding -extension () exists. This completes the contraposition and proves the lemma.
Given an encoding Π with a CI-conflict ℛ w.r.t. a positive constraint, we say ℛ is guardable if there exists a CG -extension for ℛ.
Constraint-guarding -extensions allow for the construction of problem encodings that remain consistent across all admissible instances.
and let ℛ ⊆ Π be a CI-conflict w.r.t. . Suppose ∈ ℛ, and let () be a CG -extension of w.r.t. . Let ′′ be the resulting -extended rule w.r.t. () . Then, the set ℛ ∖ {} ∪ {′′} is no longer a CI-conflict w.r.t. .
Proof. Assume that ℛ ∈ Π is a CI-conflict w.r.t. a positive constraint . By Definition 10, this implies that ℛ is compatible. Let ∈ ℛ and let () be a CG -extension for w.r.t. . Denote by ′′ the extended rule w.r.t. () , and define ℛ′ := ℛ ∖ {} ∪ {′′}. By Definition 11, () is constraint-guarding in ℛ′, implying that ℛ′ is not body-compatible Consequently, ℛ′ is not compatible and therefore not a CI-conflict w.r.t. .
Hence, robust CI-consistency can be achieved in a problem encoding by iteratively resolving all CI-conflicts through appropriate constraint-guarding -extensions.
Proposition 5. Let Π 0 be a (potentially CI-inconsistent) problem encoding and and let Ψ be a set of positive constraints. Furthermore, let all CI-conflicts in Π 0 be guardable. Then there exists a finite sequence of encodings Π 0, Π 1, . . . , Π such that for each < : • a CI-conflict ℛ ⊆ Π
w.r.t. some positive constraint ∈ Ψ is identified, and • Π +1 is obtained from Π by applying a CG -extension for a rule ∈ ℛ w.r.t. to , yielding a modified rule ′ that weakens w.r.t. the constraint-induced inconsistencies.
This process terminates after finitely many steps. The final encoding Π is then robustly CI-consistent, meaning that no constraint in Ψ can be violated under any admissible instance, and that all such constraintinduced inconsistencies have been resolved without the removal of any rule from the original encoding. Proof. We proceed by induction over the CI-conflicts in Π w.r.t. some positive constraint in Ψ.
Let Π 0 = Π. If Π 0 is already robustly CI-consistent, we are done.
Otherwise, there exists a constraint ∈ Ψ and a CI-conflict ℛ ⊆ Π 0 such that the rules in ℛ collectively allow a derivation of a set of literals that violate under some admissible instance. By assumption, not all rules in ℛ share the same body, so at least one rule ∈ ℛ admits a CG -extension ( ) for w.r.t. .
We apply ( ) to weaken w.r.t. the derivation that violates , obtaining ′. The next encoding is defined as Π 1 = Π 0 ∖ {} ∪ {′}.
This modification eliminates the particular potential constraint violation associated with the derivation of . Moreover, because the -extension reduces the derivational strength of , it cannot reintroduce the same conflict.
This process is repeated iteratively. At each step , we select a remaining unresolved CI-conflict ℛ ⊆ Π and choose a rule ∈ ℛ that can be individually weakened due to the assumption that ℛ is guardable. This guarantees progress by resolving at least one distinct conflict per step.
Since the total number of conflicts is finite (due to the finiteness of Π , Ψ , and possible derivations), the process must terminate after finitely many steps.
Let Π be the final encoding. By construction, it is robustly CI-consistent w.r.t. all constraints in Ψ (cf. Corollary 2), and every rule from the original encoding is either unchanged or replaced by a weaker version (i.e., extended rule body), without any deletions.
Algorithm 1 Constructing -Extensions for Guardable CI-conflicts Require: Encoding Π , constraint set Φ , guardable CI-conflict ℛ ⊆ Π Ensure: -extension () for some ∈ ℛ 1: Select two distinct rules , ′ ∈ ℛ 2: ← ( ′) ∖ () 3: ← { ⋆ ∈ | (⋆) ∈/ (), (⋆) ∈/ ()} 4: if = ∅ then 5: abort: no valid extended literal found 6: end if 7: Select * ∈ 8: Define 1() := {∼ ⋆} and 2() := {⋆} 9: Construct two -extended rules w.r.t. : 10: ∼ := () ← (), 1(). 11: ¬ := () ← (), 2(). 12: Select either ∼ or ¬ to replace in Π w.r.t. ∈ Ψ
To systematically enforce incompatibility within a CI-conflict, Algorithm 1 constructs a CG extension for a selected rule ∈ ′, where ℛ ⊆ Π is a guardable CI-conflict. The procedure begins by selecting a second rule ′ ∈ ℛ that the expert intends to render incompatible with (line 1). The algorithm then identifies literals ⋆ ∈ (′)∖() that do not appear in the head or body of (lines 2– 3).
choice, the algorithm constructs two possible -extensions: 1() = {∼ ⋆}, and 2() = {⋆} (line 8). These generate two -extended rule variants of , denoted by ∼ and ¬, which respectively enforce incompatibility with ′ via strong or default negation of ⋆ (lines 10–11). The expert then selects one of these -extended rules to replace the original rule (line 12). This process ensures that any resulting answer set avoids satisfying the bodies of both rules simultaneously, thereby resolving the potential constraint violation through strategic weakening.
Let us illustrate Algorithm 1 using the following example: Example 11. Let Π 11 be a problem encoding consisting of the following rules: 1: ← , ∼.
2: ← .
3: ← , ∼ℎ.
4: ← , .
5: ← , ∼.
Additionally, consider the following set Ψ 11 of constraints: 6: , , .
7: , .
The encoding Π 11 contains two CI-conflicts: ℛ 1 = {1, 2, 3} w.r.t. 6 and ℛ2 = {4, 5} w.r.t. 7.
Since the rules within each CI-conflicts do not share any atoms, both CI-conflicts are guardable.
To resolve the potential constraint violation in ℛ1, the expert selects the rule pair 1, 2, and extends 1. We define 1 = (2) ∖ (1) = { }, and thus obtain 1 = { }. Selecting , we construct possible -extensions for 1, namely 1,1 = {∼ } , and 1,2 = { }. The corresponding -extended rules for 1 are: 1∼ : ← , ∼, ∼.
1¬: ← , ∼, .
Similarly, for the CI-conflict ℛ2, we choose to extend 4. We define 2 = (5) ∖ (4) = {, ∼} , resulting in 2 = {∼} . Selecting ∼ , we construct possible -extensions for 4, namely, 2,1 = {}, and 2,2 = {∼ }. The corresponding -extended rules for 4 are: 4∼ : ← , .
4¬: ← , ∼ .
Suppose the expert selects 1∼ : and 4¬: as the -extended rules. We then obtain the following modified problem encoding Π ′11: 1∼ : ← , ∼, ∼.
Since Π ′11 contains no CI-conflicts, the modified program is CI-consistent w.r.t. Ψ
In summary, our approach provides a constructive method for ensuring robust CI-consistency. By systematically detecting CI-conflicts and resolving them through suitable constraint-guarding and informative -extensions, we isolate the sources of potential constraint violations and weaken only the necessary rules. This targeted repair strategy preserves the original encoding structure to the greatest extent possible while guaranteeing that all constraints remain satisfied under any admissible instance. As a result, the final encoding satisfies robust CI-consistency without requiring rule deletion or instance-specific modifications.
In this paper, we have introduced a novel framework for managing CI-conflicts in ELPs. By allowing users to specify coarse-grained conditions and constraints directly at the encoding level, our method automatically determines which constraints could be violated under some (unspecified) instance. We isolate the culprit rules whose derivations risk violating a constraint, leveraging the established concept of constraint-guarding -extensions, originally defined for achieving SC-consistency. Applying these -extensions yields robust CI-consistency, meaning that all constraints remain satisfied without deleting rules or depending on particular data instances.
Our main contributions are (1) a formal definition of CI-conflicts as a semantic interaction between constraints and potentially derivable literals; (2) an algorithm for detecting and characterising such conflicts at the encoding level; and (3) a constructive repair procedure based on -extensions that minimally modifies only those rules necessary to restore consistency w.r.t. constraints.
For future work, we plan to generalise our inconsistency analysis framework to accommodate all forms of constraints, including those involving default negation, thereby extending -extensions to all CI-conflicts. Furthermore, we are currently working on relaxing the current restrictions on admissible problem instances–specifically, by allowing instances to contain literals that appear in constraints.
In parallel, we are developing a complementary theory of consistency w.r.t. odd cycles for ground programs. Once this theory is established, we will investigate whether and how robust consistency w.r.t. odd cycles can be achieved. Through these developments, we aim to provide a unified, instanceindependent methodology for diagnosing and repairing all types of inconsistencies in ASP encodings.
The authors have not employed any Generative AI tools.