ASPIC compute_attacks blows up on cyclic strict rules: 4 premises, 14 rules give 18,850 arguments and ~8.7M rebuttals

[ctoth]

compute_attacks does not finish within 180 seconds on a small generated ASPIC+ theory: 8 literals, 4 ordinary premises, 11 strict rules and 3 defeasible rules. build_arguments turns this theory into 18,850 arguments in about 0.5s, and 18,496 of those arguments conclude p. The property test tests/structured/aspic/test_aspic.py::TestAttackProperties::test_rebutting_targets_defeasible_conclusions generated the theory. Hypothesis saved it in a local .hypothesis database; after that, the test hit the 600s pytest timeout on every run, and pytest then raised a MemoryError while formatting the traceback. Main CI passes this test because CI starts with an empty database.

Theory (shrunk by Hypothesis)

• Language: p, q, r, s and their negations, with each atom and its negation contradictory.
• Ordinary premises: q, s, ~p, ~r. There are no axioms.
• Strict rules:
  • p -> ~s
  • q, ~r -> s
  • q, ~s -> r
  • s -> ~p
  • ~p, ~q -> q
  • ~q, ~p -> q
  • ~q, ~q -> p
  • ~r, q -> s
  • ~r, ~s -> ~q
  • ~s, q -> r
  • ~s, ~r -> ~q
• Defeasible rules:
  • r, q => ~r (named d0)
  • s => q (named d3)
  • ~p => ~s (named d1)

Reproduction

Run with the repository development environment (uv run python repro.py), with an external timeout as the bound. At ad3c01c plus the #96 branch:

import time
from argumentation.structured.aspic.aspic import (
    ArgumentationSystem, ContrarinessFn, GroundAtom, KnowledgeBase, Literal, Rule,
    build_arguments, compute_attacks,
)
P, Q, R, S = (Literal(GroundAtom(n)) for n in "pqrs")
NP, NQ, NR, NS = (a.contrary for a in (P, Q, R, S))
strict = frozenset(Rule(b, h, "strict") for b, h in [
    ((P,), NS), ((Q, NR), S), ((Q, NS), R), ((S,), NP), ((NP, NQ), Q), ((NQ, NP), Q),
    ((NQ, NQ), P), ((NR, Q), S), ((NR, NS), NQ), ((NS, Q), R), ((NS, NR), NQ)])
defeasible = frozenset({Rule((R, Q), NR, "defeasible", "d0"),
                        Rule((S,), Q, "defeasible", "d3"),
                        Rule((NP,), NS, "defeasible", "d1")})
system = ArgumentationSystem(frozenset({P, Q, R, S, NP, NQ, NR, NS}),
    ContrarinessFn(frozenset((a, a.contrary) for a in (P, Q, R, S))), strict, defeasible)
kb = KnowledgeBase(axioms=frozenset(), premises=frozenset({Q, S, NP, NR}))
t = time.perf_counter(); args = build_arguments(system, kb)
print(len(args), "arguments", round(time.perf_counter() - t, 2), "s")
compute_attacks(args, system)  # does not return within 180 s

Operational evidence (AGENTS.md)

• build_arguments: 18,850 arguments in 0.40–0.54s.
• Arguments per conclusion: p 18,496, r 144, ~q 136, s 31, q 18, ~r 17, ~p 4, ~s 4.
• Rebut attack points (a sub-argument whose top rule is defeasible): 98,849. Rebutting attack pairs: 8,687,712. This counts rebuttals only; undermining pairs are extra.
• compute_attacks still had not returned when killed at 180s.
• Profile: py-spy, 30s at 50 Hz on the real interpreter rather than the uv launcher, 1,499 samples. The top leaf frames are compute_attacks at aspic.py:1159–1164, the loop that adds one attack_keys entry per (attack point, candidate attacker) pair, with Argument.__hash__ (aspic.py:249) behind it. The cost is the size of the attack relation itself, not one slow step.

The underlying shape is argument multiplication. Cyclic strict rules, including ones with a repeated antecedent (~q, ~q -> p) and mirrored bodies (~p, ~q -> q / ~q, ~p -> q), give p 18,496 structurally distinct arguments. Each rebuttable sub-argument then pairs with every argument for the contrary conclusion.

Expected

The finite theory should be decided within a bounded budget, or the test generators should not produce theories whose argument sets explode. Which of those, if either, is a design decision for this issue. A useful first operational contract would be to bound len(build_arguments(...)) and the attack-pair count on this theory, so the regression fails fast instead of timing out.

No production change is included in this report.

[ctoth]

Investigation: evidence, papers and fix options

No production change yet. All probes ran on main 052775e.

Evidence

• The cost is the size of the output, not a slow algorithm. compute_attacks already indexes attackers by conclusion: candidate_attackers is built once per target literal, so there is no pairwise scan to remove. A py-spy profile on the real interpreter confirms the report above: all the time is in the loop that emits one attack at a time (aspic.py:1159-1164), plus Argument.__hash__. Measured cost is about 3.3 µs per emitted attack: a variant of this theory with 800 arguments and 569,330 attacks took 1.9 s in compute_attacks.

• The attack relation is larger than reported above. Counted without materialising it, from per-conclusion argument counts:

  • rebutting pairs: 8,687,712
  • undermining pairs: 297,283,248

  About 306M Attack objects is roughly 17 minutes at the measured rate, plus several GB of memory, whatever algorithm produces them.

• Where the arguments multiply: of the 18,850 arguments, 18,496 conclude p. That is exactly 136²: the rule ~q, ~q -> p combines two independent ~q arguments, and there are 136 of them. Permuted duplicate rules multiply further: ~p,~q -> q and ~q,~p -> q, and ~r,~s -> ~q and ~s,~r -> ~q.

  Variant	Arguments	Rebutting pairs	Undermining pairs
  as is	18,850	8,687,712	297,283,248
  merge permuted duplicate strict rules only	800	49,646	519,684
  remove the repeated antecedent literal only (~q,~q -> p becomes ~q -> p)	490	94,824	139,592
  both (antecedents read as a set)	98	2,936	4,290

• How the test generator produced this theory: strict_rules() in tests/structured/aspic/test_aspic.py draws antecedents with replacement, which gave the seed ~q,~q -> p. transposition_closure keeps antecedent positions, so that one seed became the two permuted rules (~p,~q) -> q and (~q,~p) -> q.

Papers

• Modgil & Prakken 2018 Def 5 (p.9) and Prakken 2010 Def 3.6 build an argument A1, ..., An -> φ from a rule Conc(A1), ..., Conc(An) -> φ. Neither requires arguments to be minimal. The only construction-time filter is c-consistency (M&P Def 11), and build_arguments already applies it. Under this sequence reading, ~q,~q -> p applied to two different ~q arguments is a genuinely distinct argument, whose premise set is the union of both.
• M&P Def 27 defines premise-minimal arguments. But Prop 28, that restricting to them leaves extensions unchanged, is proven only under a particular condition on the argument ordering. So pruning by minimality changes semantics in general.
• Merging clones (arguments with the same conclusion, the same Prem, DefRules and LastDefRules, and the same attack points including sub-argument strengths) only reduces the count to 7,459.

Operational contract

On this theory, assert len(build_arguments(...)) <= 200, and assert that the attack-pair count, computed from per-conclusion counts without calling compute_attacks, is at most 20,000. This is deterministic and runs in under a second. Today it fails at 18,850 arguments and about 306M pairs. Under option A it would pass at 98 arguments and 7,226 pairs.

Fix options

• A (recommended; needs a semantic decision): canonicalise rules as antecedent sets.
  • A1: treat strict rules with the same antecedent set and consequent as one rule. This only removes clone arguments (same Prem, DefRules and attack points), so extensions are unchanged up to clones. 18,850 → 800 arguments.
  • A2: also remove repeated antecedent literals. This drops arguments that combine different sub-arguments for the same antecedent literal, which changes which arguments exist under the sequence reading. 18,850 → 98 arguments.
  • Defeasible rules stay distinct by name in both.
• B: quotient by argument clones. Semantics-preserving, but it only reaches 7,459 arguments and millions of attacks. Not recommended.
• C: keep only premise-minimal arguments (M&P Def 27). 28 arguments, but not semantics-preserving under preferences (Prop 28's condition). Only if that reading is wanted.

Separate test-only fix (PR to follow, Refs #102)

• The generators draw distinct antecedents in a canonical order.
• The attack property tests discard examples with more than 2,000 arguments, so a saved theory can't be replayed into a timeout.
• This theory is pinned with the contract above, marked xfail(strict=True) until option A lands.

[ctoth]

Decision recorded: strict-rule antecedents are read as sets (option A1 + A2)

The maintainer chose option A1 + A2 from the investigation above. The fix is in PR #104 (branch fix/aspic-rule-sets).

Convention. Modgil & Prakken 2018, Def 2 (p.8) and Def 5 (p.9), and Prakken 2010, Def 3.6, write a rule as φ1, ..., φn → φ and build an argument A1, ..., An → φ from it. Neither text fixes whether the antecedents form a sequence or a set. This library now chooses the set reading for strict rules, as a convention:

• A repeated antecedent literal is dropped, so ~q, ~q → p is the rule ~q → p.
• Strict rules with the same antecedent set and consequent are one rule (~p, ~q → q and ~q, ~p → q are the same rule).
• Defeasible rules keep their antecedent sequence and stay distinct by name n(r).

Semantic effect:

• A1, merging permuted duplicate strict rules: this removes only clone arguments, which have the same premises, defeasible rules and attack points. A property test confirms that grounded, complete, preferred and stable extensions are unchanged up to clones.
• A2, dropping repeated antecedents: under the sequence reading, ~q, ~q → p built one argument for p per ordered pair of ~q arguments. Those combined arguments no longer exist; there is one argument per ~q argument. This is the deliberate semantic change.

Where it lives. The canonicalisation happens in Rule.__post_init__, at rule construction. As a result, every producer gets the same reading without any per-producer code: transposition_closure, Datalog grounding, hand-built systems and ABA rules.

Producer audit:

• Datalog grounding: two authored strict rules whose bodies are the same set ground to one rule, and both source ids are kept (Datalog projection loses source provenance when distinct strict rules ground identically #67).
• transposition_closure emits canonical rules.
• The ASPIC+ ASP encoding already counted distinct antecedents (ASPIC ASP backend fails to derive rules with repeated antecedents #64).
• The ABA ASP body_count is consistent, because ABA strict rules are now canonical. A probe of a defeasible rule with a repeated antecedent also agrees between the native and ASP backends.

Result on the #102 theory: 18,850 → 98 arguments, and about 306M → 7,226 attack pairs. The pinned operational contract (at most 200 arguments and at most 20,000 attack pairs) now passes, and its xfail marker is removed.

[ctoth]

Decision extended by the maintainer: the set reading now applies to defeasible rules too (PR #104). A repeated antecedent literal is dropped, and unnamed defeasible rules with the same antecedent set and consequent merge. Named defeasible rules stay distinct by n(r), so undercuts still target the named rule. Canonicalisation happens once, in Rule.__post_init__, for every rule kind. Full suite: 3511 passed, 7 skipped, 1 xfailed.