Follow Modgil & Prakken 2018 Def 14 on mixed attack/defeat frameworks

src/argumentation/core/dung.py

@@ -174,15 +174,67 @@ def admissible(
 
 
 def grounded_extension(framework: ArgumentationFramework) -> frozenset[str]:
-    """Compute the unique grounded extension.
+    """Compute the unique grounded extension: the least complete extension.
 
-    This is pure Dung grounded semantics: the least fixed point of the
-    characteristic function over ``defeats`` only. Attack metadata is
-    ignored here.
+    The characteristic function uses ``defeats``. Its least fixed point G is
+    contained in every complete extension, since each is a fixed point of it.
+    On a single-relation framework G is the Dung grounded extension. When
+    ``attacks`` differ from ``defeats``, conflict-freeness is measured on
+    attacks (Modgil & Prakken 2018, Def 14): G is then the least complete
+    extension if it is conflict-free on attacks, and otherwise no complete
+    extension exists, so a ``ValueError`` is raised instead of returning a
+    conflicting set. :func:`grounded_extensions` returns ``()`` instead.
 
     References:
         Dung 1995, Definition 20 + Theorem 25 (least fixed point).
+        Modgil & Prakken 2018, Definition 14.
+    """
+    extensions = grounded_extensions(framework)
+    if not extensions:
+        raise ValueError(
+            "framework has no complete extension: the least fixed point of the "
+            "defeat-based characteristic function is not conflict-free on "
+            "attacks (Modgil & Prakken 2018, Def 14), and every complete "
+            "extension would contain it"
+        )
+    return extensions[0]
+
+
+def grounded_extensions(
+    framework: ArgumentationFramework,
+) -> tuple[frozenset[str], ...]:
+    """Return ``(grounded,)``, or ``()`` when no complete extension exists.
+
+    The tuple form matches :func:`extensions_for`: like complete and stable,
+    grounded has no extension on a mixed framework whose defeat-based least
+    fixed point conflicts on attacks (Modgil & Prakken 2018, Def 14).
     """
+    least_fixed_point = _defeat_least_fixed_point(framework)
+    if framework.attacks is not None and not conflict_free(
+        least_fixed_point, framework.attacks
+    ):
+        return ()
+    return (least_fixed_point,)
+
+
+def attacks_resolved_by_defeats(framework: ArgumentationFramework) -> bool:
+    """Whether every attack is a defeat in at least one direction.
+
+    Holds for every single-relation framework. On such mixed frameworks the
+    defeat-based least fixed point is conflict-free on attacks and contained
+    in every Def 14 admissible-maximal set, so grounded-based shortcuts and
+    reducts stay sound; without it they can be unsound (issue #90).
+    """
+    if framework.attacks is None:
+        return True
+    return all(
+        edge in framework.defeats or (edge[1], edge[0]) in framework.defeats
+        for edge in framework.attacks
+    )
+
+
+def _defeat_least_fixed_point(framework: ArgumentationFramework) -> frozenset[str]:
+    """Least fixed point of the characteristic function over ``defeats``."""
     attackers_index = predecessors_index(framework.defeats)
     targets_index = successors_index(framework.defeats)
     live_attackers = {
@@ -269,20 +321,83 @@ def preferred_extensions(framework: ArgumentationFramework) -> list[frozenset[st
     """
     if framework.attacks is None or framework.attacks == framework.defeats:
         return maximal_sets(complete_extensions(framework))
-    attackers_index = predecessors_index(framework.defeats)
-    return maximal_sets(
-        [
-            candidate
-            for candidate in _all_subsets(framework.arguments)
+    extensions, _nodes = _mixed_preferred_search(framework)
+    return extensions
+
+
+def _mixed_preferred_search(
+    framework: ArgumentationFramework,
+) -> tuple[list[frozenset[str]], int]:
+    """Maximal Def 14 admissible sets of a mixed framework, and the node count.
+
+    Depth-first search over arguments in sorted order, trying ``in`` before
+    ``out``. A branch is cut when (1) an ``in`` argument has a defeater that
+    no remaining candidate can defeat, so no completion is admissible;
+    (2) every set the branch can still reach is contained in an admissible
+    set already found, so it cannot yield a new maximal one; or (3) an
+    ``out`` argument conflicts with nothing reachable and is already defended
+    by the ``in`` arguments, so adding it to any completion stays admissible
+    and no completion is maximal. Conflict-freeness uses attacks, defense uses
+    defeats (Modgil & Prakken 2018, Def 14). The node count is exposed for the
+    operational contract tests.
+    """
+    attacks = framework.attacks if framework.attacks is not None else framework.defeats
+    order = sorted(framework.arguments)
+    conflicts: dict[str, set[str]] = {argument: set() for argument in order}
+    for source, target in attacks:
+        conflicts[source].add(target)
+        conflicts[target].add(source)
+    defeaters = predecessors_index(framework.defeats)
+    found: list[frozenset[str]] = []
+    nodes = 0
+    # Explicit stack instead of recursion: depth equals the argument count.
+    stack: list[tuple[int, frozenset[str], frozenset[str]]] = [
+        (0, frozenset(), frozenset())
+    ]
+    while stack:
+        index, chosen, excluded = stack.pop()
+        nodes += 1
+        reachable = chosen | frozenset(
+            argument
+            for argument in order[index:]
+            if argument not in conflicts[argument] and not conflicts[argument] & chosen
+        )
+        if any(reachable <= extension for extension in found):
+            continue
+        if not all(
+            any(
+                candidate in defeaters.get(defeater, frozenset())
+                for candidate in reachable
+            )
+            for argument in chosen
+            for defeater in defeaters.get(argument, frozenset())
+        ):
+            continue
+        if any(
+            argument not in conflicts[argument]
+            and not conflicts[argument] & reachable
+            and all(
+                defeaters.get(defeater, frozenset()) & chosen
+                for defeater in defeaters.get(argument, frozenset())
+            )
+            for argument in excluded
+        ):
+            continue
+        if index == len(order):
             if admissible(
-                candidate,
+                chosen,
                 framework.arguments,
                 framework.defeats,
                 attacks=framework.attacks,
-                attackers_index=attackers_index,
-            )
-        ]
-    )
+                attackers_index=defeaters,
+            ):
+                found.append(chosen)
+            continue
+        argument = order[index]
+        stack.append((index + 1, chosen, excluded | {argument}))
+        if argument not in conflicts[argument] and not conflicts[argument] & chosen:
+            stack.append((index + 1, chosen | {argument}, excluded))
+    return maximal_sets(found), nodes
 
 
 def stable_extensions(framework: ArgumentationFramework) -> list[frozenset[str]]:
@@ -689,10 +804,11 @@ def extensions_for(
     """Return extensions for the supported Dung semantics.
 
     Single-extension semantics (grounded, ideal) are returned as a 1-tuple so
-    every semantics yields a uniform ``tuple[frozenset[str], ...]``.
+    every semantics yields a uniform ``tuple[frozenset[str], ...]``. Grounded
+    is ``()`` when the framework has no complete extension (Def 14).
     """
     if semantics == "grounded":
-        return (grounded_extension(framework),)
+        return grounded_extensions(framework)
     if semantics == "complete":
         return tuple(complete_extensions(framework))
     if semantics == "preferred":

src/argumentation/core/preprocessing.py

@@ -60,6 +60,7 @@
 
 from argumentation.core.dung import (
     ArgumentationFramework,
+    attacks_resolved_by_defeats,
     grounded_extension,
 )
 from argumentation.core.finite import predecessors_index, successors_index
@@ -130,7 +131,13 @@ def simplify_af(
     removal is). When ``semantics`` is ``None`` the grounded reduct is applied --
     callers are responsible for only calling this for supported semantics.
     """
-    apply_grounded = semantics is None or semantics in GROUNDED_REDUCT_SEMANTICS
+    # On a mixed framework with an attack that is a defeat in neither direction,
+    # the defeat-based grounded set need not be conflict-free on attacks or
+    # contained in every extension (Modgil & Prakken 2018, Def 14; issue #90),
+    # so the grounded reduct is only applied when every attack is resolved.
+    apply_grounded = (
+        semantics is None or semantics in GROUNDED_REDUCT_SEMANTICS
+    ) and attacks_resolved_by_defeats(framework)
 
     fixed_in: frozenset[str] = frozenset()
     fixed_out: frozenset[str] = frozenset()

src/argumentation/core/scc_recursive.py

@@ -56,6 +56,7 @@
     _strongly_connected_components,
     _subframework,
     admissible,
+    attacks_resolved_by_defeats,
     characteristic_fn,
     complete_extensions,
     preferred_extensions,
@@ -289,6 +290,17 @@ def scc_extensions(
     LAST_SOLVE.semantics = semantics
     LAST_SOLVE.decompose_requested = decompose
 
+    if not attacks_resolved_by_defeats(framework):
+        # SCCs are taken over defeats, so an attack that is a defeat in neither
+        # direction can link SCCs the recursion treats as independent, and the
+        # base preferred (maximal complete) differs from Def 14 preferred
+        # (maximal admissible) there (Modgil & Prakken 2018, Def 14; issue #90).
+        LAST_SOLVE.flat_fast_path = True
+        LAST_SOLVE.notes.append(
+            "attack that is a defeat in neither direction -> flat Def 14 solve"
+        )
+        return _flat_enumerate(semantics, framework)
+
     if not decompose:
         LAST_SOLVE.flat_fast_path = True
         LAST_SOLVE.notes.append("decompose=False -> flat base solve on whole AF")

src/argumentation/semantics.py

@@ -17,7 +17,7 @@
     ArgumentationFramework,
     cf2_extensions,
     complete_extensions,
-    grounded_extension,
+    grounded_extensions,
     ideal_extension,
     preferred_extensions,
     prudent_grounded_extension,
@@ -70,7 +70,7 @@ def _dung_extensions(
     semantics: str,
 ) -> tuple[frozenset[str], ...]:
     if semantics == "grounded":
-        return (grounded_extension(framework),)
+        return grounded_extensions(framework)
     if semantics == "ideal":
         return (ideal_extension(framework),)
     if semantics == "complete":

src/argumentation/solver_adapters/iccma_af.py

@@ -13,7 +13,7 @@
     admissible,
     characteristic_fn,
     conflict_free,
-    grounded_extension,
+    grounded_extensions,
     range_of,
 )
 from argumentation.interop.iccma import write_af
@@ -380,7 +380,7 @@ def _validate_witness_certificate(
             raise ICCMAOutputParseError("complete witness is not a complete extension")
         return
     if semantics == "grounded":
-        if witness != grounded_extension(framework):
+        if (witness,) != grounded_extensions(framework):
             raise ICCMAOutputParseError(
                 "grounded witness is not the grounded extension"
             )

src/argumentation/solving/af_sat.py

@@ -11,6 +11,7 @@
 
 from argumentation.core.dung import (
     ArgumentationFramework,
+    attacks_resolved_by_defeats,
     grounded_extension,
     range_of,
 )
@@ -920,6 +921,11 @@ def _shortcut(self, query: str) -> bool | None:
                 "preferred_skeptical_shortcut_self_attacking_query", False
             )
             return False
+        if not attacks_resolved_by_defeats(self.framework):
+            # The remaining shortcuts assume every preferred extension contains
+            # the defeat-based grounded set, which fails when an attack is a
+            # defeat in neither direction (Modgil & Prakken 2018, Def 14).
+            return None
         attackers = self._attackers_of(query)
         if not attackers:
             self._emit_shortcut("preferred_skeptical_shortcut_unattacked_query", True)

src/argumentation/solving/sat_encoding.py

@@ -11,7 +11,7 @@
 from argumentation.core.dung import (
     ArgumentationFramework,
     admissible,
-    grounded_extension,
+    grounded_extensions,
     ideal_extension,
     semi_stable_extensions,
     stage_extensions,
@@ -34,7 +34,7 @@ def sat_extensions(
     if semantics == "admissible":
         return _sorted_extensions(_admissible_sets(framework))
     if semantics == "grounded":
-        return (grounded_extension(framework),)
+        return grounded_extensions(framework)
     # complete / preferred / stable -> SCC-recursive layer (Wave B2): grounded-reduct
     # preprocessing composed with Baroni-Giacomin-Guida SCC decomposition. Transparent.
     if semantics in ("complete", "preferred", "stable"):

src/argumentation/solving/solver.py

@@ -33,9 +33,10 @@
 from argumentation.structured.aspic.aspic import Literal
 from argumentation.core.dung import (
     ArgumentationFramework,
+    attacks_resolved_by_defeats,
     cf2_extensions,
     complete_extensions,
-    grounded_extension,
+    grounded_extensions,
     ideal_extension,
     preferred_extensions,
     semi_stable_extensions,
@@ -391,7 +392,13 @@ def solve_dung_single_extension(
         if sat is not None and sat.require_external:
             return _external_sat_unavailable()
         trace_sink, metadata, check_budget_seconds = _sat_options(sat)
-        find_single = _SAT_SINGLE_EXTENSION_FINDERS.get(semantics)
+        # The dedicated SAT kernels assume every attack is a defeat in some
+        # direction; otherwise use the Def 14 enumeration below (issue #90).
+        find_single = (
+            _SAT_SINGLE_EXTENSION_FINDERS.get(semantics)
+            if attacks_resolved_by_defeats(framework)
+            else None
+        )
         if find_single is not None:
             # Only complete/preferred finders accept an engine and are routed to
             # sat-core (SE-CO / SE-PR); stable/semi-stable/stage/ideal keep smt.
@@ -453,7 +460,10 @@ def solve_dung_acceptance(
         if sat is not None and sat.require_external:
             return _external_sat_unavailable()
         trace_sink, metadata, check_budget_seconds = _sat_options(sat)
-        if requested_backend == "auto":
+        # The cone and dedicated SAT kernels assume every attack is a defeat in
+        # some direction; otherwise use the Def 14 enumeration (issue #90).
+        dedicated_kernels_apply = attacks_resolved_by_defeats(framework)
+        if requested_backend == "auto" and dedicated_kernels_apply:
             # Query-directed SCC-cone path (sound per the derivations in
             # experiments/2026-07-10-af-scc-acceptance.md); None means the
             # cone does not apply or is inconclusive -> flat path below.
@@ -473,7 +483,11 @@ def solve_dung_acceptance(
                 return _optional_dependency_unavailable(exc)
             if cone_result is not None:
                 return cone_result
-        solve_dedicated = _dedicated_sat_acceptance_solver(semantics, task)
+        solve_dedicated = (
+            _dedicated_sat_acceptance_solver(semantics, task)
+            if dedicated_kernels_apply
+            else None
+        )
         if solve_dedicated is not None:
             try:
                 return solve_dedicated(
@@ -1157,7 +1171,7 @@ def _dung_extensions(
     semantics: str,
 ) -> list[frozenset[str]]:
     if semantics == "grounded":
-        return [grounded_extension(framework)]
+        return list(grounded_extensions(framework))
     # complete / preferred / stable: route through the SCC-recursive layer
     # (Wave B2), which composes the Wave A grounded-reduct preprocessing with
     # Baroni-Giacomin-Guida SCC decomposition. Transparent: identical results,

src/argumentation/structured/aspic/aspic_encoding.py

@@ -141,6 +141,10 @@ def solve_aspic_grounded(
     This is the tested direct package query surface. Its current backend is the
     materialized ASPIC-to-Dung reference path; optional ASP/clingo backends can
     attach to the same encoding/result contract in later slices.
+
+    Raises ``ValueError`` when the projected framework has no complete
+    extension, which happens only outside Modgil & Prakken 2018's well-defined
+    domain (Def 14; e.g. strict rules not closed under transposition).
     """
     from argumentation.core.dung import grounded_extension
 
@@ -420,7 +424,7 @@ def _materialized_extensions(framework, semantics: str) -> tuple[frozenset[str],
     from argumentation.core import dung
 
     if semantics == "grounded":
-        return (dung.grounded_extension(framework),)
+        return dung.grounded_extensions(framework)
     if semantics == "admissible":
         return tuple(
             candidate