[Rule] SetSplitting to NAESatisfiability

[isPANN]

Source

SetSplitting

Target

NAESatisfiability

Motivation

Set Splitting is precisely hypergraph two-colorability, while NAE-SAT expresses the same condition clause by clause. This missing reverse edge complements the existing NAE-SAT to Set Splitting rule and connects the source directly to a logical decision model.

Reference

Garey and Johnson, Computers and Intractability, 1979, Appendix A (Set Splitting); Schaefer, “The Complexity of Satisfiability Problems,” STOC 1978 (NAE relations).

Reduction Algorithm

Given universe U={0,...,n-1} and subset vectors S_0,...,S_{m-1}, each of length at least two:

1. Create Boolean variable x_u for every u in U; its truth value denotes the side of the split. Encode positive literal x_u as the signed, 1-indexed CNFClause value (u + 1) as i32.
2. For every subset vector S_j, retain the first occurrence of each distinct element, preserving order. If at least two distinct elements remain, create one NAE clause containing their positive literals. If the only distinct element is u, create the clause (x_u,x_u).
3. Extract the split directly from the truth assignment: element u receives the side represented by x_u.

Removing repeated occurrences does not change whether a subset contains elements from both sides. After canonicalization, a subset with at least two distinct elements is split exactly when its NAE clause has both truth values. A subset whose entries all equal u is unsplittable and becomes the unsatisfiable NAE clause (x_u,x_u). Thus the construction and direct extraction preserve YES and NO instances in both directions.

Size Overhead

Target metric	Formula
num_vars	universe_size
num_clauses	num_subsets
num_literals	(universe_size + 1) * num_subsets

The literal formula is an upper bound. The exact number is the sum, over all source subset vectors, of the number of distinct elements, except that a vector with only one distinct element contributes two literal occurrences.

Validation Method

• Enumerate every two-way split and every Boolean assignment and compare them configuration by configuration.
• Test repeated members, unused universe elements, empty families, and subsets of sizes 2, 3, and larger.
• Check that each emitted clause has at least two literals, uses only valid 1-indexed variable identifiers, and satisfies the stated size bounds.
• The canonical example was exhaustively checked over all 16 assignments.

Example

1. Source instance: U={0,1,2,3} with subsets [{0,1},{1,2,3},{0,2,3}].
2. Construction: variables x_0,...,x_3 and NAE clauses (x_0,x_1), (x_1,x_2,x_3), (x_0,x_2,x_3), encoded respectively as (1,2), (2,3,4), and (1,3,4).
3. Target witness: assignment [0,1,0,1].
4. Round trip: the subsets evaluate respectively to [0,1], [1,0,1], and [0,0,1], so all are split. Assignments such as [0,0,0,1] fail the first subset, making the example sensitive to omitted clauses.
5. NO edge case: for U={0} and subset vector [0,0], canonicalization emits (x_0,x_0), encoded as (1,1). Both assignments make its literals equal, so both source and target are infeasible.

BibTeX

@inproceedings{Schaefer1978,
  author = {Schaefer, Thomas J.},
  title = {The Complexity of Satisfiability Problems},
  booktitle = {Proceedings of the Tenth Annual ACM Symposium on Theory of Computing},
  pages = {216--226},
  year = {1978},
  doi = {10.1145/800133.804350}
}

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	pred path SetSplitting NAESatisfiability --json reports no path; a GitHub title search found no duplicate proposal other than this issue.
Non-trivial	✅ Pass	The rule translates a set-family feasibility instance into logical NAE constraints, constructing one target clause per source subset and preserving witnesses.
Correctness	✅ Pass	Both references exist and support the problem semantics; exhaustive testing confirmed the pointwise equivalence on 57,929 small configurations.
Completeness	✅ Pass	The construction covers every instance admitted by the source model, including repeated members, empty families, unused elements, and clauses larger than three.
Well-written	❌ Fail	The stated num_literals = universe_size * num_subsets upper bound is false because the source model permits repeated members and the algorithm explicitly preserves them.

Overall: 4 passed, 1 failed, 0 warnings

---

Usefulness

Both names resolve through pred show. There is currently no reduction path from SetSplitting to NAESatisfiability; the reverse primitive edge exists, but it does not make this direction redundant. A repository-wide rule search found only SetSplitting → ILP and SetSplitting → Betweenness, and the GitHub duplicate search returned only #1100. The motivation explains the practical graph connection and why the direct logical edge matters.

Non-trivial

This is not a subtype cast, same-problem variant conversion, or variable-complement substitution. It converts each source set constraint into a target CNFClause, changes the instance representation, and gives a direct witness map. Although the semantic equivalence is simple, the issue provides a complete constraint construction rather than an identity/coercion.

Correctness

• Garey and Johnson, Computers and Intractability (1979), Appendix A3.1, SP4, printed p. 221, defines Set Splitting for a collection of subsets of a finite set and asks for a two-part partition such that no member is contained wholly in either part. It also identifies the problem as hypergraph 2-colorability and records the connection from NOT-ALL-EQUAL 3SAT.
• Schaefer, “The Complexity of Satisfiability Problems” (STOC 1978), DOI 10.1145/800133.804350, printed p. 217, defines NP2 NOT-ALL-EQUAL SATISFIABILITY as two-coloring sets of at most three members so that no set is monochromatic. Theorem 2.1 and the discussion following it establish the NP-completeness background for the NAE relation. The title, author, year, pages, and DOI match the project bibliography and the paper.
• These are independent sources for the same local predicate: a source subset is split iff the corresponding tuple of positive Boolean literals contains both truth values. Schaefer's named NP2 presentation is arity-at-most-three, but the issue does not rely on that bound: the repository target model accepts every clause of length at least two, and the same pointwise predicate applies at arbitrary arity.
• A temporary brute-force checker compared the source and target value configuration-by-configuration for universes through size 3, subset sequences of lengths 2–4 (including repetitions), and families of up to two subsets: 57,929 configurations passed. The four-variable canonical witness also passed.

No newer or lower-overhead construction is relevant here: the direct representation change already uses one variable per universe element and one clause per source subset.

Completeness

Literature scope. Garey–Johnson SP4 states the source for arbitrary finite subset collections, with no connectedness, coverage, or bounded-arity precondition. Schaefer's NP2 statement uses sets of size at most three, but that restriction is used for its complexity result, not by this issue's direct predicate-preserving construction. For every source set S_j, regardless of size, the construction enforces exactly “the colors on S_j are not all equal.”

Codebase scope. SetSplitting::try_new accepts any universe size and any family whose member vectors have length at least two and contain in-range indices; it permits repetitions, unused universe elements, empty families, and sets longer than three. NAESatisfiability::try_new accepts arbitrary clause lengths of at least two. The target's size fields are num_vars, num_clauses, and num_literals. Existing SetSplitting → ILP preserves repeated terms and has an explicit {0,0} infeasibility test; SetSplitting → Betweenness also begins from arbitrary source subset vectors via normalization.

Hand traces beyond the worked example:

1. U = ∅, empty family: the construction produces zero variables and zero clauses. Both source and target are vacuously satisfied by the empty configuration; extraction returns the empty split.
2. U = {0}, family [{0,0}]: the target is the repeated-literal NAE clause (x_0,x_0). Both assignments make its two literal values equal, so the target is unsatisfiable, exactly matching the unsplittable source member.
3. An unused universe element creates an unconstrained target variable and remains an unconstrained choice in the extracted split. A member of length greater than three becomes an equally long NAE clause, which the target model supports.

The construction therefore preserves semantics on all source instances admitted by the codebase.

Well-written

All required sections are present, symbols are introduced, target metric names match pred show NAESatisfiability --json, the extraction map is clear, and the four-variable example is non-degenerate. Exhaustive enumeration shows four satisfying assignments, and for each of the three clauses there is an assignment that violates only that clause, so omitted-clause bugs are observable.

One implementability error must be fixed. The issue says repeated source members are retained, but then claims

num_literals ≤ universe_size * num_subsets.

This is not an upper bound for the actual Rust source type Vec<Vec<usize>>. For example, universe_size = 2 and the legal single member [0,0,0,0,1] produce five literal occurrences, while the claimed bound is 2 × 1 = 2. Repetition length is unbounded by the two listed source metrics.

Recommendations

• Canonicalize each member before clause construction: emit each distinct element once; if only one distinct element remains, emit (x_u,x_u) as the fixed unsatisfiable clause. Then a bound such as (universe_size + 1) * num_subsets is valid using existing source getters.
• Alternatively, add and use a source size getter for total membership occurrences. Without one of these changes, the declared overhead cannot describe the proposed algorithm.
• State the concrete code encoding u ↦ (u + 1) as i32 because CNFClause literals are signed and 1-indexed.

[isPANN]

Rule Fix

Diagnosis:

• Overhead consistency: the original num_literals = universe_size * num_subsets claim was not an upper bound because the source model permits arbitrarily many repeated occurrences in a subset vector. For example, universe size 2 with [0,0,0,0,1] emitted five literals against a claimed bound of two.
• The reduction direction, two correctness directions, direct solution extraction, polynomial construction, Or-to-Or type compatibility, examples, and target-instance validity were otherwise sound.

Literature:

• Garey and Johnson's Set Splitting formulation and Schaefer's NAE relation both use the same non-monochromatic predicate. The direct one-subset-to-one-clause construction agrees with that canonical equivalence; the issue diverged only by preserving duplicate occurrences while claiming a bound based on universe size and subset count.
• The Schaefer DOI metadata and repository bibliography were verified. The ACM-hosted paper was access-blocked during this run, so the comparison also used the existing page-level source verification already recorded on this issue.

Changes:

• Canonicalize each source subset vector to its distinct elements before clause construction.
• Preserve an all-repeated unsplittable subset as the valid unsatisfiable clause (x_u,x_u).
• State the concrete signed, 1-indexed encoding u -> (u + 1) as i32.
• Replace the invalid literal bound with (universe_size + 1) * num_subsets and state the exact occurrence count.
• Add explicit target-validity checks and a worked NO edge case.

Smoke test:

• 192 checks passed across all mandatory buckets: YES example, NO example, edge cases, 64 feasibility-agreement instances, witness extraction, four overhead spot-checks, and target validity.
• Key confirming instances included the empty family, an unused variable, [0,0] over a one-element universe, and [0,0,0,0,1] over a two-element universe.

[isPANN]

Issue Quality Re-check — Rule

Check	Result	Details
Usefulness	✅ Pass	pred path SetSplitting NAESatisfiability --json still reports no path, and the title search finds no duplicate beyond #1100.
Non-trivial	✅ Pass	The rule constructs one logical NAE constraint per source subset and defines a witness-preserving representation change.
Correctness	✅ Pass	The canonical non-monochromatic equivalence is preserved after deduplication, including all-repeated subsets via (x_u,x_u); 192 smoke checks passed.
Completeness	✅ Pass	The edited construction covers every instance accepted by SetSplitting, including repeated members, empty families, unused elements, and unbounded subset arity.
Well-written	✅ Pass	The invalid literal bound is replaced by a valid repository-expressible upper bound, and the encoding, exact count, extraction, and NO edge case are explicit.

Overall: 5 passed, 0 failed, 0 warnings

Previously: 4 passed and 1 failed. The sole failure, the false num_literals upper bound, is resolved.

---

Usefulness

Both model names resolve via pred show. There is no existing reduction path in this direction; the reverse primitive edge does not make this proposal redundant. A GitHub title search returns only this issue. The motivation explains the value of the direct logical connection.

Non-trivial

The construction is not a subtype cast or same-problem identity. It transforms each set-family constraint into a CNFClause, canonicalizes source vectors where representation-level duplicates occur, and gives a direct target-to-source witness map.

Correctness

• Garey and Johnson, Computers and Intractability (1979), Appendix A3.1, SP4, defines Set Splitting as a two-part partition in which no member is wholly contained in either part and records its hypergraph two-coloring interpretation.
• Schaefer, “The Complexity of Satisfiability Problems” (STOC 1978), DOI 10.1145/800133.804350, defines the not-all-equal relation as requiring both colors within each constraint. Its metadata matches docs/paper/references.bib.
• Deduplicating repeated occurrences preserves the set of truth values present in a constraint. When only one distinct element remains, (x_u,x_u) is NAE-unsatisfiable exactly when the source subset vector is unsplittable.
• The corrected construction passed 192 checks: the worked YES and NO cases, four edge cases, 64 feasibility comparisons, 49 extraction checks, four overhead checks, and 68 target-validity checks.

No lower-overhead construction is relevant: the rule already uses one variable per universe element and one clause per source subset.

Completeness

Literature scope. Garey–Johnson's source formulation is over arbitrary finite subset collections. Schaefer's named NP2 presentation has bounded arity for its complexity theorem, but the local not-all-equal predicate used here applies at every arity supported by the repository target.

Codebase scope. SetSplitting::try_new accepts empty families, unused universe elements, repeated entries, and subset vectors longer than three, provided each vector has length at least two and every index is in range. NAESatisfiability::try_new accepts arbitrary clause lengths of at least two. The edited algorithm handles these cases as follows:

1. Empty universe and empty family produce zero variables and clauses; both instances are vacuously feasible.
2. U={0} with [0,0] produces (1,1); both sides are infeasible.
3. Unused elements remain unconstrained variables and survive direct extraction.
4. Long subset vectors become clauses over their distinct elements, with no arity restriction beyond the target model's minimum length.

Well-written

All required sections are present and substantive. The target size metrics match pred show NAESatisfiability --json. The signed 1-indexed literal encoding is explicit, the two canonicalization branches are implementable, both correctness directions are stated, and solution extraction is unambiguous.

The bound (universe_size + 1) * num_subsets is valid: a canonicalized clause has at most universe_size literals when at least two distinct elements remain, while the one-distinct-element case has exactly two literals; for a nonempty family the source validation implies universe_size >= 1. The body also states the exact per-clause occurrence count.