Modularity Aspects of Disjunctive Stable Models

1. Introduction

• Stable models are not readily compositional, and prior module-theorem work restricted positively interdependent atom definitions to a single module.The paper extends modularity analysis to disjunctive programs under stable-model semantics.Source: §1 · p. 2
• Modularizing stable-model search may help with large instances and query evaluation, but computing module stable models separately is not necessarily efficient.The introduction identifies independently computed modules and their later linking as a setting requiring care about communication costs.Source: §1 · pp. 2–3
• Modularization also bears on optimization and verification, while contemporary disjunctive answer-set solvers are described as offering little support for modular reasoning.The introduction notes incremental solving and correctness proofs as further applications of modular results.Source: §1 · p. 3
• DLP-functions provide modules with explicit input, output, and hidden atoms, supporting systematic composition while allowing shared rules under relaxed syntactic restrictions.The paper extends modular-program theory for normal and smodels programs to disjunctive programs.Source: §1 · p. 3
• The module theorem characterizes whole-program stable models as unions of compatible module stable models and uses positive-dependency strongly connected components to constrain composition.The theorem generalizes the splitting-set theorem and is proved using completion and loop formulas.Source: §1 · p. 4
• The paper applies the framework to QBF representation, generalized shifting of shared disjunctive rules, decomposition, and modular equivalence for program comparison.The shifting generalization partially covers programs involving head-cycles; modular equivalence also supports substitutions and translation-based verification.Source: §1 · p. 4

2. The Class of DLP-Functions

• A DLP-function packages rules with distinct input, output, and hidden atom sets; its rules may use inputs but must define outputs or hidden atoms, not inputs alone.Input and output atoms are visible to other modules, while hidden atoms serve auxiliary concepts that may not make sense outside the module.Source: §2 · pp. 5–6
• Composition requires interface-respect conditions because unrestricted program union does not guarantee compositional semantics.The conditions include restrictions on hidden atoms, output atoms, and the distribution of rules defining outputs.Source: §2 · p. 6
• Unlike normal programs, disjunctive modules may share rules whose heads define outputs of both modules; those defining rules must remain intact in the union.The example shares the rule a ∨ b ← c; disjunctive heads can create dependencies between atoms, unlike independent choices in choice rules.Source: §2 · pp. 6–7
• The composition operator unions rules and signatures, removes from the combined inputs atoms supplied as outputs, and retains the modules’ hidden atoms.The figure summarizes the resulting atom categories, including which atoms may originate in both modules.Source: §2 · p. 8
• A DLP-function is intended to map input subsets to sets of output-and-hidden-atom subsets, with its formal semantics deferred to the next section.The interface notation also supports projections onto input, output, visible, and hidden atoms.Source: §2 · p. 9
• Positive-dependency strongly connected components determine mutual dependence; the join is composition restricted to mutually independent modules.The dependency graph excludes input atoms because their definitions are external to the DLP-function.Source: §2 · p. 9

Classical models and input

• Classical models evaluate rules under an interpretation; input atoms are treated as fixed values through partial evaluation of the DLP-function.Instantiation removes the input signature and reduces rules according to the actual input.Source: §3 · pp. 10–11

Minimal and stable models

• I-minimal models minimize a model while holding its input atoms fixed, providing the minimality notion used to define stable models.Classical and minimal models serve as auxiliary concepts; stable models are the intended semantics.Source: §3 · pp. 10, 12

Stable models

• A stable model of a DLP-function is an input-minimal model of its reduct, with negative body literals handled by the Gelfond–Lifschitz transformation.For ordinary disjunctive programs without inputs, this reduces to minimality of the reduct.Source: §3 · pp. 12–13
• For any fixed input, projecting a stable model onto output and hidden atoms yields a stable model of the input-instantiated DLP-function.This provides a way to avoid explicitly requiring input-minimality in the stable-model definition.Source: §3 · p. 13

Example 3.10

• With input signature {c}, the example has four stable models: {a}, {b}, {a, c}, and {b, c}.The stable models associated with each actual input form a local antichain, although the full set need not be an antichain.Source: §3 · pp. 13–14
• The example’s instantiated functions have stable models {a} and {b} for both inputs {c} and ∅.These are the stable models of Π/{c} and Π/∅, respectively.Source: §3 · p. 13

4. Characterizations using Classical Logic

• Completion and loop formulas are generalized to DLP-functions, incorporating input atoms into classical-logic characterizations of stable models.The section also extends tightness to DLP-functions by defining it relative to the input signature.Source: §4 · p. 14

4.1 Program Completion and Loop Formulas

• A DLP-function interpretation is stable exactly when it satisfies both its completion and its loop formulas.Loops are non-empty subsets of strongly connected components in the positive dependency graph over output and hidden atoms.Source: §4.1 · pp. 14–15

4.2 Tight DLP-functions

• For a tight DLP-function, the classical models of its completion characterize its stable models.Tightness means the positive dependency graph, which excludes input atoms, is acyclic.Source: §4.2 · pp. 16–17

5.1 Module Theorem

• Stable models of a defined join are exactly the unions of compatible stable models of its modules; positively interdependent atoms must remain in the same module.The result extends to any finite sequence of modules whose join is defined, with pairwise compatibility ensuring each module model can be recovered by projection.Source: §5.1 · pp. 21–22
• The theorem extends composition from two modules to any finite sequence, and the example with three modules yields stable models {a, b}, {a, c}, and {b, c}.For the extension, module interpretations must be pairwise compatible.Source: §5.1 · pp. 21–22

5.2 Modular Representation of Quantified Boolean Formulas

• The QBF encoding uses an upper DLP-function to explain clause activations and a lower DLP-function as a coNP oracle for unsatisfiability checks.The evaluation problem is Σp 2-complete, matching the complexity of checking whether a disjunctive program has a stable model.Source: §5.2 · pp. 22, 24
• For the illustrated QBF instance, the input activating all four clauses yields a positive answer, with {x1} as the explanation and the formula valid.The explanation assigns x1 true and x2 false, making the remaining matrix true for all assignments to y1 and y2.Source: §5.2 · p. 24
• Each stable model of Πsat_n is determined by its projection onto X, which is minimal among interpretations meeting the act(i) conditions, with no relevant assignments lost.Source: §5.2 · p. 25
• A QBF ∃X∀Y φ of form (19) is valid exactly when Πsat_n has at least one stable model.Source: §5.2 · p. 25

5.3 Splitting Sets

• For mutual-negation rules, splitting sets apply only trivially, whereas Theorem 5.7 permits separate module models to compose and also accommodates input atoms.Source: §5.3 · p. 27

6. Decomposing DLP-Functions

• Rules whose heads intersect multiple SCCs may be included in the defining rules for more than one component.Integrity constraints are not assigned to an SCC module.Source: §6 · p. 28
• The decomposition uses an extra module Π0 to retain integrity constraints and input atoms absent from R’s rules, while its other modules are induced by SCCs.Each ΠS uses At(DefR(S)) \ S as its input signature and provides defining rules, if any, for atoms in S.Source: §6 · p. 28
• When distinct SCC modules fail to respect each other's hidden atoms, grouping connected components into maximal blocks restores that respect between resulting modules.Conflicts can also involve Π0 when its integrity constraints refer to a module's hidden atoms; constraints involving a block's hidden atoms are redistributed to that block.Source: §6 · p. 30
• The hidden-atom-aware decomposition can collapse several SCCs into one module, as when hiding a and c connects all three components in the example.With H = {a, c}, the example's decomposition becomes a single module ΠS′ = Π.Source: §6 · p. 31
• The example suggests prioritizing modules with few stable models and combining modules that share few visible atoms.The remaining modules in the example merely approve the two models obtained from the other modules.Source: §6 · p. 31

7. Shifting Disjunctions

• Local shifting can change stable models when a disjunctive rule's head intersects an SCC in multiple atoms, as with a ∨ b ∨ c ← and the cycle a ← b, b ← a.The example has SM(Π1) = {{a, b}, {c}} but SM(Π2) = {{c}} after local shifting.Source: §7 · p. 32
• General shifting projects each disjunctive rule's head onto each SCC it intersects and shifts the other head atoms into that component's negative body.It is applied with the SCC-based decomposition to address cases where local shifting fails in the presence of head-cycles.Source: §7 · p. 32
• General shifting preserves the stable models of the example with a ∨ b ∨ c ← and the cycle a ← b, b ← a, unlike local shifting.For Π1, SM(GSH(Π1)) = {{a, b}, {c}} = SM(Π1), whereas SM(Π2) = {{c}}.Source: §7 · p. 32
• SM(Π) = SM(GSH(Π)) for any DLP-function Π, including those with hidden atoms.The proof reveals hidden atoms for decomposition and then hides them again.Source: §7 · p. 34
• Duplicating shared disjunctive rules across SCC modules can create up to n copies of a rule body; a new atom naming the body can partly reduce this blow-up.The stated worst case is quadratic space; dencode can decide whether introducing a body atom pays off.Source: §7 · p. 34

8.1 Modular Equivalence

• Modular equivalence compares compatible DLP-functions through a bijection between stable models that preserves their visible atoms.Compatibility requires matching input and output signatures.Source: §8.1 · p. 35
• Modular equivalence is preserved when both functions are composed with a context, provided the joins are defined.Thus, equivalent components can be substituted within a larger DLP-function.Source: §8.1 · p. 35

8.2 Verifying Modular Equivalence

• The paper's translation-based verification method adjusts prior weak-equivalence checking to account for input semantics and hidden atoms.For ordinary disjunctive programs, the resulting translation coincides with the earlier translation of Oikarinen and Janhunen (2004).Source: §8.2 · pp. 36, 38
• The verification theorem applies when compatible DLP-functions have enough visible atoms: they are modularly equivalent iff both directional translations have no stable models.Enough visible atoms means the hidden part has a unique stable model for each visible input interpretation.Source: §8.2 · pp. 36, 38
• The context-composition test uses the same two directional emptiness checks, and its context need not have enough visible atoms.It is required only that both component-context joins be defined.Source: §8.2 · p. 38

9. Related Work

• Eiter et al. (1997a) use disjunctive datalog query programs with no recursion between modules, while allowing a partial order of modules.Their approach accounts for positive and negative dependencies; the paper notes that partial orders of DLP-functions are permitted by join.Source: §9 · p. 39
• This paper follows programming-in-the-large, which constructs programs from modules using algebraic operators such as join, unlike programming-in-the-small's abstraction mechanisms.The latter approach is illustrated by nested generalized-quantifier modules in Eiter et al. (1997b).Source: §9 · p. 39
• The module theorem generalizes the splitting-set theorem, while Faber et al. (2007)'s module theorem is described as a special case of it.Their result uses independent sets, which are splitting sets, though not every splitting set is independent.Source: §9 · p. 40

• The framework models disjunctive logic programs as DLP-functions with input/output interfaces and definitions tailored to disjunctive-rule characteristics.Source: §10 · p. 40
• The module theorem is proved for DLP-functions generally, covering disjunctive programs and providing compositional semantics that generalizes splitting-set and magic-set approaches.Source: §10 · p. 40
• It supports decomposition into components to localize reasoning, and generalized shifting can remove shared disjunctive rules even with head-cycles, at potentially higher space cost.Source: §10 · p. 40
• The theory of modular equivalence applies to DLP-functions.Source: §10 · p. 40
• The authors anticipate practical engineering uses: decomposition and linking tools exist for smodels, dencode implements general shifting, and lpeq supports modular equivalence for smodels.Source: §10 · pp. 40–41