From 0a3289757d1b441223703f58f76a2835454f1b08 Mon Sep 17 00:00:00 2001 From: Christopher Toth Date: Sun, 27 Sep 2026 06:54:59 -0600 Subject: [PATCH] fix: reject underivable queries in incremental ABA skeptical preferred In an assumption-free framework with no rule for q, supported(q) is not a ground atom. is_skeptically_accepted_preferred still passed it to clingo as a false assumption; clingo reports UNSAT for an assumption on an absent atom (potassco/clingo#671), which the counterexample search read as skeptical acceptance. An ungrounded query is now answered directly: no assumption set derives it, so the answer is False with a preferred extension as counterexample. The credulous helpers get the same guard. Native, SAT and support-reference routes were already correct; the ASP and auto acceptance routes inherited the incremental bug. Closes #72 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01V4tAVyyKcs1sYcsEzL7Bzg --- .../structured/aba/aba_incremental.py | 20 +++ .../aba/test_aba_skeptical_underivable.py | 123 ++++++++++++++++++ 2 files changed, 143 insertions(+) create mode 100644 tests/structured/aba/test_aba_skeptical_underivable.py diff --git a/src/argumentation/structured/aba/aba_incremental.py b/src/argumentation/structured/aba/aba_incremental.py index fae10d6..d9b2b2f 100644 --- a/src/argumentation/structured/aba/aba_incremental.py +++ b/src/argumentation/structured/aba/aba_incremental.py @@ -404,6 +404,16 @@ def _symbol_supported(self, literal: Literal): return None return self._clingo.Function("supported", [self._clingo.Function(literal_id)]) + @staticmethod + def _is_grounded(ctl, symbol) -> bool: + """Whether ``symbol`` is an atom of the grounded program. + + ``supported(s)`` is grounded only if some rule can derive ``s``; an + absent atom is false in every model and must not be passed to clingo + as an assumption (potassco/clingo#671). + """ + return symbol in ctl.symbolic_atoms + def _extract_in_set(self, model) -> AssumptionSet: # MUST be called only inside the on_model callback -- clingo Model objects # are invalid afterwards. @@ -604,6 +614,12 @@ def is_skeptically_accepted_preferred( # Any preferred set is a counterexample; produce one. return False, self.find_preferred_extension(telemetry=telemetry) ctl = self._new_control(telemetry=telemetry) + if not self._is_grounded(ctl, query_symbol): + # No rule can derive the query, so no assumption set derives it and + # every preferred set is a counterexample. Assuming the absent atom + # false must not reach clingo: it reports UNSAT (potassco/clingo#671), + # which would read as skeptical acceptance. + return False, self.find_preferred_extension(telemetry=telemetry) permanently_unsat = {"flag": False} def add_refinement(out_set: frozenset[Literal]) -> bool: @@ -728,6 +744,8 @@ def is_credulously_accepted_complete( if query_symbol is None: return False, None ctl = self._new_control() + if not self._is_grounded(ctl, query_symbol): + return False, None witness = self._solve_one(ctl, assumptions=[(query_symbol, True)]) if witness is None: return False, None @@ -740,6 +758,8 @@ def is_credulously_accepted_stable( if query_symbol is None: return False, None ctl = self._new_control(extra_program=":- out(X), not defeated(X).") + if not self._is_grounded(ctl, query_symbol): + return False, None witness = self._solve_one(ctl, assumptions=[(query_symbol, True)]) if witness is None: return False, None diff --git a/tests/structured/aba/test_aba_skeptical_underivable.py b/tests/structured/aba/test_aba_skeptical_underivable.py new file mode 100644 index 0000000..83b0089 --- /dev/null +++ b/tests/structured/aba/test_aba_skeptical_underivable.py @@ -0,0 +1,123 @@ +"""Skeptical acceptance of literals no rule can derive (issue #72). + +A literal is in an extension's closure only if rules derive it from the +assumptions (Bondarenko et al. 1997, Th(T), p.69). Lehtonen et al. 2021 +(Sec 4.2.3) decide skeptical acceptance by searching for a counterexample +that does not derive the query: UNSAT means accepted. When ``supported(q)`` +is not a ground atom at all, no set derives q, so a counterexample always +exists; clingo's negative assumption on an absent atom must not be read as +UNSAT (potassco/clingo#671). +""" + +from __future__ import annotations + +import pytest +from hypothesis import given, settings +from hypothesis import strategies as st + +from argumentation.solving.solver import solve_aba_acceptance +from argumentation.structured.aba import aba +from argumentation.structured.aspic.aspic import GroundAtom, Literal, Rule +from tests.aba_hypothesis_generators import flat_aba_frameworks + +pytest.importorskip("clingo") + +from argumentation.structured.aba.aba_asp import solve_aba_with_backend # noqa: E402 + +Q = Literal(GroundAtom("q")) + + +def _assumption_free(rules: frozenset[Rule] = frozenset()) -> aba.ABAFramework: + return aba.ABAFramework(frozenset({Q}), rules, frozenset(), {}) + + +@pytest.mark.parametrize("simplify", [False, True]) +def test_incremental_skeptical_preferred_rejects_underivable_literal( + simplify: bool, +) -> None: + """Issue #72: the only preferred extension is {}, whose closure lacks q, + so q is not skeptically accepted and {} is the counterexample.""" + framework = _assumption_free() + assert set(aba.preferred_extensions(framework)) == {frozenset()} + assert not aba.derives(framework, frozenset(), Q) + + result = solve_aba_with_backend( + framework, + backend="asp", + semantics="preferred", + task="skeptical", + query=Q, + simplify=simplify, + ) + + assert result.answer is False + assert result.counterexample == frozenset() + assert int(result.metadata["solver_calls"]) <= 2 + + +@pytest.mark.parametrize("backend", ["native", "sat", "asp", "auto"]) +@pytest.mark.parametrize("semantics", ["complete", "preferred", "stable"]) +@pytest.mark.parametrize("task", ["credulous", "skeptical"]) +def test_every_acceptance_route_rejects_underivable_literal( + backend: str, + semantics: str, + task: str, +) -> None: + """Issue #72: no route may accept q when nothing derives it.""" + result = solve_aba_acceptance( + _assumption_free(), + semantics=semantics, + task=task, + query=Q, + backend=backend, + ) + + assert result.answer is False # type: ignore[union-attr] + + +@pytest.mark.parametrize("backend", ["native", "sat", "asp", "auto"]) +@pytest.mark.parametrize("semantics", ["complete", "preferred", "stable"]) +@pytest.mark.parametrize("task", ["credulous", "skeptical"]) +def test_every_acceptance_route_accepts_derivable_fact_control( + backend: str, + semantics: str, + task: str, +) -> None: + """Issue #72 control: with the fact rule -> q, q is in the closure of the + empty extension, so every route accepts it.""" + framework = _assumption_free(frozenset({Rule((), Q, "strict")})) + + result = solve_aba_acceptance( + framework, + semantics=semantics, + task=task, + query=Q, + backend=backend, + ) + + assert result.answer is True # type: ignore[union-attr] + + +@given( + flat_aba_frameworks(min_assumptions=0, max_assumptions=0, max_rules=5), + st.sampled_from(["complete", "preferred", "stable"]), + st.sampled_from(["credulous", "skeptical"]), +) +@settings(max_examples=60, deadline=None) +def test_asp_acceptance_matches_native_on_assumption_free_frameworks( + framework: aba.ABAFramework, + semantics: str, + task: str, +) -> None: + """Issue #72 guard: the audit's failures were all assumption-free, so for + every language literal the ASP route must agree with the native reference + on generated assumption-free frameworks (the regression itself is pinned + by the explicit cases above).""" + for query in sorted(framework.language, key=repr): + native = solve_aba_acceptance( + framework, semantics=semantics, task=task, query=query, backend="native" + ) + asp = solve_aba_acceptance( + framework, semantics=semantics, task=task, query=query, backend="asp" + ) + assert asp.answer is native.answer # type: ignore[union-attr]