[Model] MinimumAxiomSet

[isPANN]

Motivation

MINIMUM AXIOM SET (P269) from Garey & Johnson, A9 LO17. A generalization of Set Cover with multi-level deductive closure via implication rules. Given a set of sentences, a set of true sentences, and implication rules, find the smallest subset of true sentences whose deductive closure equals the full set of true sentences.

Associated rules:

• [Rule] X3C to MinimumAxiomSet #870: ExactCoverBy3Sets → MinimumAxiomSet (NP-completeness proof, Pudlák 1975)

Structural connections:

• Generalizes MinimumSetCovering (single-antecedent implications reduce to Set Cover)
• Equivalent to Minimum Generating Set for a closure system
• Equivalent to Minimum Source Set on directed hypergraphs

Definition

Name: MinimumAxiomSet
Reference: Garey & Johnson, Computers and Intractability, A9 LO17

Mathematical definition:

INSTANCE: Finite set S of "sentences," subset T ⊆ S of "true sentences," an "implication relation" R consisting of pairs (A, s) where A ⊆ S and s ∈ S.
OBJECTIVE: Find the minimum-size subset S₀ ⊆ T whose deductive closure under R equals T.

The deductive closure is computed iteratively: S₀ ⊆ S₁ ⊆ ... ⊆ Sₙ where Sᵢ = Sᵢ₋₁ ∪ {s : ∃U ⊆ Sᵢ₋₁, (U, s) ∈ R}, until fixpoint Sₙ = Sₙ₊₁.

Variables

• Count: |T| (one binary variable per candidate axiom in T)
• Per-variable domain: binary {0, 1}
• Meaning: y_s = 1 if sentence s is selected as an axiom in S₀. Minimize |S₀| = Σ y_s such that the deductive closure of S₀ equals T.

Schema (data type)

Type name: MinimumAxiomSet
Variants: none

Field	Type	Description
num_sentences	usize	Total number of sentences
true_sentences	Vec<usize>	Indices of true sentences T ⊆ S
implications	Vec<(Vec<usize>, usize)>	Implication rules: (antecedent set A, consequent s)

Notes:

• This is an optimization problem: Value = Min<usize>.
• Key getter methods: num_sentences() (= |S|), num_true_sentences() (= |T|), num_implications() (= |R|).

Complexity

• Decision complexity: NP-complete (Pudlák, 1975; transformation from X3C). NP-complete even if T = S.
• Best known exact algorithm: O*(2^|T|) brute force — enumerate all subsets of T, compute deductive closure for each (polynomial per subset via fixpoint).
• Concrete complexity expression: "2^num_true_sentences" (for declare_variants!)
• Approximation: O(log |T|) via greedy (analogous to Set Cover greedy).
• References:
  • P. Pudlák (1975). "Polynomially complete problems in the logic of automated discovery." MFCS 1975.

Extra Remark

Full book text:

INSTANCE: Finite set S of "sentences," subset T⊆S of "true sentences," an "implication relation" R consisting of pairs (A,s) where A⊆S and s∈S, and a positive integer K≤|S|.
QUESTION: Is there a subset S_0⊆T with |S_0|≤K and a positive integer n such that, if we define S_i, 1≤i≤n, to consist of exactly those s∈S for which either s∈S_{i-1} or there exists a U⊆S_{i-1} such that (U,s)∈R, then S_n=T?
Reference: [Pudlák, 1975]. Transformation from X3C.
Comment: Remains NP-complete even if T=S.

How to solve

• It can be solved by (existing) bruteforce. (Enumerate subsets of T by increasing size; compute deductive closure; return smallest whose closure = T.)
• It can be solved by reducing to integer programming. (Binary variable per sentence; layered indicator variables for fixpoint; minimize Σ y_s. Companion rule issue to be filed separately.)
• Other: Greedy approximation (O(log |T|) ratio).

Example Instance

Input:
S = {a, b, c, d, e, f, g, h} (8 sentences), T = S (all true)

Implication rules:

1. ({a}, c) — a → c
2. ({a}, d) — a → d
3. ({b}, e) — b → e
4. ({b}, f) — b → f
5. ({c, e}, g) — c ∧ e → g (multi-antecedent)
6. ({d, f}, h) — d ∧ f → h (multi-antecedent)
7. ({g, h}, a) — g ∧ h → a
8. ({g, h}, b) — g ∧ h → b

Optimal axiom set (size 2): S₀ = {a, b}

• Step 0: {a, b}
• Step 1: a → c, d; b → e, f. S₁ = {a, b, c, d, e, f}
• Step 2: {c, e} → g; {d, f} → h. S₂ = {a, b, c, d, e, f, g, h} = T ✓

Optimal value: Min(2) — 2 solutions exist: {a, b} and {g, h}.

Second solution: S₀ = {g, h}

• Step 0: {g, h}
• Step 1: {g, h} → a; {g, h} → b. S₁ = {a, b, g, h}
• Step 2: a → c, d; b → e, f. S₂ = {a, b, c, d, e, f, g, h} = T ✓

Why size 1 is insufficient:

• {a}: closure = {a, c, d} (cannot reach e, f, g, h)
• {b}: closure = {b, e, f} (cannot reach c, d, g, h)
• {g} or {h} alone: no rules fire (both need the other as co-antecedent)
• Other singletons: no rules have them as sole antecedent

Python validation script

from itertools import combinations

rules = [
    ({0}, 2), ({0}, 3), ({1}, 4), ({1}, 5),
    ({2, 4}, 6), ({3, 5}, 7), ({6, 7}, 0), ({6, 7}, 1),
]
T = set(range(8))

def closure(axioms):
    current = set(axioms)
    changed = True
    while changed:
        changed = False
        for ante, cons in rules:
            if ante.issubset(current) and cons not in current:
                current.add(cons); changed = True
    return current

for k in range(9):
    found = [c for c in combinations(range(8), k) if closure(c) == T]
    if found:
        assert k == 2
        names = "abcdefgh"
        print(f"Min axiom set: {k} ({len(found)} solutions)")
        for f in found:
            print(f"  {{{', '.join(names[i] for i in f)}}}")
        break

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	✅ Pass	Novel problem not yet in reduction graph; planned reductions mentioned
Non-trivial	✅ Pass	Distinct feasibility constraints (deductive closure via multi-antecedent implications)
Correctness	⚠️ Warn	References verified but complexity bound is only brute-force 2^
Well-written	❌ Fail	Missing Expected Outcome in example; ILP claimed but no companion rule issue linked; second optimal solution {g,h} omitted

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

Pass. MinimumAxiomSet does not exist in the codebase (pred show MinimumAxiomSet fails). The issue mentions concrete structural connections to existing problems:

• Generalizes MinimumSetCovering (already implemented) — single-antecedent implications reduce to Set Cover.
• NP-completeness via reduction from X3C (G&J reference R213).
• Equivalent to Minimum Generating Set for closure systems and Minimum Source Set on directed hypergraphs.

These provide clear pathways to connect this problem to the existing reduction graph.

Non-trivial

Pass. The problem has genuinely distinct feasibility constraints from all existing problems. The defining feature is the multi-level deductive closure via implication rules with multi-antecedent sets — this is structurally different from MinimumSetCovering (which is single-level coverage) because the closure operator is not union-closed: cl(A ∪ B) ⊋ cl(A) ∪ cl(B) is possible. No existing problem in the codebase captures this iterative fixpoint semantics.

Correctness

Warn. Reference verification results:

1. Pudlák (1975), "Polynomially complete problems in the logic of automated discovery," MFCS 1975: Verified — the paper exists in MFCS 1975 proceedings (Springer LNCS), pp. 358–361. It establishes NP-completeness of the Minimum Axiom Set problem. ✅

2. Lucchesi & Osborn (1978), "Candidate keys for relations," JCSS 17(2), pp. 270–279: Verified — already in the project bibliography (lucchesi1978keys). The paper shows that deciding whether a key of cardinality ≤ K exists is NP-complete, confirming the connection to the single-antecedent special case. ✅

3. Complexity bound: The issue claims O(2^|T| · poly(|S|, |R|)) brute force. This is correct but trivial — it is simply exhaustive enumeration with no algorithmic insight. The issue does not cite any improved exact algorithm with a better exponential base. For a problem from G&J, a literature search for faster exact algorithms would strengthen the complexity section. ⚠️

4. Definition correctness: The mathematical definition matches the G&J book text (provided verbatim in the "Extra Remark" section). The deductive closure fixpoint iteration is correctly specified. ✅

5. ILP formulation claim: The issue claims the problem "can be solved by reducing to integer programming" with "layered indicator variables," but encoding a fixpoint computation in ILP requires careful linearization (the number of layers is bounded by |T|, so this is feasible but non-trivial). The claim is plausible. ✅

Well-written

Fail. Several issues found:

1. Missing Expected Outcome (Fail): The Example Instance section shows the construction and explains why K=2 works and K=1 does not, but does not provide a clearly labeled "Expected Outcome" with the optimal objective value. It should explicitly state: "Optimal value: Min(2), optimal solution: S₀ = {a, b}."

2. Missing companion ILP rule issue (Fail): The "How to solve" section checks the ILP box and describes a reduction approach, but per project conventions, when direct ILP solving is claimed, the issue must link a companion [Rule] MinimumAxiomSet to ILP issue. No such issue exists or is referenced.

3. Incomplete example — second optimal solution omitted (Warn): Python verification confirms there are exactly 2 optimal solutions at K=2: {a, b} and {g, h}. The issue only mentions {a, b} and does not acknowledge {g, h}. The closure of {g, h}: rules 7,8 fire → {a,b,g,h} → rules 1-4 fire → {a,b,c,d,e,f,g,h} = T. For paper quality, both should be mentioned.

4. Complexity section lacks concrete expression (Warn): The complexity section should provide a concrete complexity expression in terms of problem parameters (e.g., "2^num_true_sentences") suitable for the declare_variants! macro, not just big-O prose.

5. Example quality — round-trip testability (Pass): The example has 8 sentences, 8 implication rules, K_opt=2, with 2 optimal solutions and 20 suboptimal feasible solutions at K=3. This is rich enough for meaningful round-trip testing. ✅

6. Schema and definition (Pass): All fields are well-defined, types are appropriate (Vec<(Vec<usize>, usize)> for implications), and the Min<usize> value type is correct for a minimization problem. ✅

7. Naming (Pass): MinimumAxiomSet follows the Minimum prefix convention for minimization problems. ✅

Recommendations

• Add a concrete complexity expression like "2^num_true_sentences" for declare_variants!.
• File a companion [Rule] MinimumAxiomSet to ILP issue and link it, or remove the ILP checkbox.
• Mention both optimal solutions {a,b} and {g,h} in the example, and add an explicit "Expected Outcome: Min(2)" line.
• Consider searching for improved exact algorithms beyond brute-force 2^n enumeration.

[isPANN]

Converted from decision framing (bound K) to optimization framing (minimize axiom set size). Removed bound field from schema. Updated definition, variables, and example to use optimization language. Removed PoorWritten label.

[isPANN]

Fix-issue changelog

• Associated rules: Linked [Rule] X3C to MinimumAxiomSet #870 (X3C → MinimumAxiomSet).
• Example: Added second optimal solution {g,h} with step-by-step derivation. Added explicit "Why size 1 is insufficient" analysis.
• Complexity: Added concrete expression "2^num_true_sentences".
• Schema notes: Added Value = Min<usize> and getter methods.
• ILP: Added companion rule note.
• Added Python validation script confirming Min(2) with 2 solutions.

Applied by /fix-issue.