[Rule] X3C to MinimumAxiomSet

[isPANN]

Source: X3C
Target: MINIMUM AXIOM SET

Motivation: Establishes NP-completeness of Minimum Axiom Set via reduction from Exact Cover by 3-Sets. Minimum Axiom Set generalizes Set Cover by adding multi-level deductive closure — selecting axiom A may enable deriving sentence B, which then enables deriving C via a chain of implications. This makes it strictly harder than Set Cover in the general case and connects to Horn logic forward chaining, abductive reasoning, and directed hypergraph reachability.

Reference: Garey & Johnson, Computers and Intractability, Appendix A9.2, p.263

GJ Source Entry

[LO17] MINIMUM AXIOM SET
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 E 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 E S for which either s E S_{i-1} or there exists a U ⊆ S_{i-1} such that (U,s) E R, then S_n = T?
Reference: [Pudlák, 1975]. Transformation from X3C.
Comment: Remains NP-complete even if T = S.

Reduction Algorithm

Reference: [Pudlák, 1975]. Transformation from X3C.

Summary:
Given an X3C instance — universe U = {u₁,...,u₃q}, collection C = {C₁,...,Cₘ} of 3-element subsets of U — construct a Minimum Axiom Set instance as follows:

1. Sentences: S = U ∪ C (one sentence per universe element and one per set in the collection)
2. True sentences: T = S (all sentences are true; the comment in G&J confirms NP-completeness for T = S)
3. Implication rules: For each set Cⱼ = {uₐ, uᵦ, u_c} ∈ C, add:
   • ({Cⱼ}, uₐ) — "if Cⱼ is an axiom, then uₐ is derived"
   • ({Cⱼ}, uᵦ) — "if Cⱼ is an axiom, then uᵦ is derived"
   • ({Cⱼ}, u_c) — "if Cⱼ is an axiom, then u_c is derived"
4. Threshold: K = q (the number of 3-sets needed for an exact cover)

Correctness:

• An exact cover of U uses exactly q sets from C, covering all 3q elements.
• Selecting these q sets as axioms: each set-sentence Cⱼ derives its 3 elements via the implication rules. Since T = S and all set-sentences are also in the axiom set, the deductive closure from the q axiom-sets plus the derived elements covers all of S.
• Wait — we also need the set-sentences themselves to be in the closure. Since T = S and we only pick q set-sentences as axioms, the remaining m − q set-sentences must be derivable. This requires additional implication rules.

Refined construction (ensuring all set-sentences are derivable):

• Add implication rules: for each Cⱼ = {uₐ, uᵦ, u_c}, add ({uₐ, uᵦ, u_c}, Cⱼ) — "if all three elements of Cⱼ are known true, then Cⱼ is derived"
• This creates a two-level closure: axiom sets → their elements → other sets whose elements are all covered → (possibly more elements, but in X3C each element is in the cover exactly once)

Solution extraction: The axiom set S₀ ⊆ T with |S₀| = q corresponds to an exact cover {Cⱼ : Cⱼ ∈ S₀} of U.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_sentences	3q + m (3q universe elements + m sets)
num_true_sentences	3q + m (T = S)
num_implications	3m + m = 4m (3 element-derivation rules + 1 set-derivation rule per set)
threshold	q

Validation Method

• Closed-loop test: reduce an X3C instance, solve Minimum Axiom Set with BruteForce, extract the axiom set, verify it forms an exact cover
• Verify deductive closure: starting from axiom set S₀, iterate implication rules until fixpoint, check S_n = T
• Test with both solvable and unsolvable X3C instances
• Test edge case: T = S (the G&J comment guarantees NP-completeness for this case)

Example

Source instance (X3C):
Universe: U = {1, 2, 3, 4, 5, 6} (q = 2)
Collection:

• C₁ = {1, 2, 3}
• C₂ = {1, 4, 5}
• C₃ = {3, 5, 6}
• C₄ = {2, 4, 6}
• C₅ = {1, 3, 5}

Exact cover: {C₅, C₄} = {1,3,5} ∪ {2,4,6} = {1,2,3,4,5,6} ✓.

Constructed target instance (Minimum Axiom Set):

Sentences: S = {1, 2, 3, 4, 5, 6, C₁, C₂, C₃, C₄, C₅} (11 sentences)
True sentences: T = S (all are true)
Threshold: K = 2

Implication rules:

• ({C₁}, 1), ({C₁}, 2), ({C₁}, 3), ({1,2,3}, C₁)
• ({C₂}, 1), ({C₂}, 4), ({C₂}, 5), ({1,4,5}, C₂)
• ({C₃}, 3), ({C₃}, 5), ({C₃}, 6), ({3,5,6}, C₃)
• ({C₄}, 2), ({C₄}, 4), ({C₄}, 6), ({2,4,6}, C₄)
• ({C₅}, 1), ({C₅}, 3), ({C₅}, 5), ({1,3,5}, C₅)

Deductive closure from axioms S₀ = {C₅, C₄}:

• Step 0: S₀ = {C₅, C₄}
• Step 1: Derive from C₅ → {1,3,5}; derive from C₄ → {2,4,6}. S₁ = {C₅, C₄, 1, 2, 3, 4, 5, 6}
• Step 2: {1,2,3} all known → derive C₁. {1,4,5} all known → derive C₂. {3,5,6} all known → derive C₃. S₂ = {C₅, C₄, 1, 2, 3, 4, 5, 6, C₁, C₂, C₃} = S = T ✓

Minimum axiom set of size K=2 exists: {C₅, C₄}, corresponding to exact cover {C₅, C₄} of U.

Why K=1 is insufficient: No single set covers all 6 elements, so no single axiom can derive all of T through the closure.

References

• [Pudlák, 1975]: [Pudlak1975] P. Pudlák (1975). "Polynomially complete problems in the logic of automated discovery". In: Mathematical Foundations of Computer Science. Springer.