[Rule] NOT-ALL-EQUAL 3SAT to PARTITION INTO PERFECT MATCHINGS

[isPANN]

Source: NOT-ALL-EQUAL 3SAT
Target: PARTITION INTO PERFECT MATCHINGS

Motivation: This is the canonical reduction establishing NP-completeness of PARTITION INTO PERFECT MATCHINGS, due to Schaefer (1978). It encodes the not-all-equal constraint using graph gadgets where a 2-colorable perfect matching (K=2 case) corresponds to a satisfying NAE assignment.
Reference: Garey & Johnson, Computers and Intractability, A1.1 GT16

GJ Source Entry

[GT16] PARTITION INTO PERFECT MATCHINGS
INSTANCE: Graph G = (V,E), positive integer K ≤ |V|.
QUESTION: Can the vertices of G be partitioned into k ≤ K disjoints sets V_1, V_2, . . . , V_k such that, for 1 ≤ i ≤ k, the subgraph induced by V_i is a perfect matching (consists entirely of vertices with degree one)?
Reference: [Schaefer, 1978b]. Transformation from NOT-ALL-EQUAL 3SAT.
Comment: Remains NP-complete for K = 2 and for planar cubic graphs.

Reduction Algorithm

Summary:
Given a NAESatisfiability instance with n variables x_1, ..., x_n and m clauses C_1, ..., C_m (each clause has exactly 3 literals), construct a PartitionIntoPerfectMatchings instance (G, K=2) as follows. The key idea is Schaefer's "2-colorable perfect matching" formulation: can the vertices of G be 2-colored so that every vertex has exactly one same-color neighbor?

Gadget construction:

1. Variable gadget: For each variable x_i, create a pair of vertices (t_i, f_i) connected by an edge. In a valid 2-coloring, t_i and f_i must receive the same color (they are each other's unique same-color neighbor). The color assigned to this pair represents the truth value of x_i: color 0 = TRUE, color 1 = FALSE.

   However, to allow variables to appear in multiple clauses, we need a variable-copying gadget (also called an equality gadget). This gadget forces two vertex pairs to carry the same truth assignment. For each occurrence of variable x_i in a clause, create a separate copy of the variable pair and link copies via equality gadgets.

2. Equality (copy) gadget: To force two variable-pair nodes (a, b) to carry the same color assignment, introduce intermediate vertices and edges that constrain the 2-coloring so that the two pairs must agree. The specific construction uses a small fixed graph that enforces equality of the color patterns.

3. Clause gadget (NAE constraint): For each clause C_j = (l_1, l_2, l_3), use a K_4 (complete graph on 4 vertices) gadget. The K_4 has vertices {w_1, w_2, w_3, w_4}. In any valid 2-coloring of K_4 where each vertex has exactly one same-color neighbor, the 4 vertices split into 2 pairs of same-color vertices. This means exactly 2 of the 3 literal vertices connected to the gadget share one color and 1 has the other -- enforcing the not-all-equal condition. The three literal connections are wired to w_1, w_2, w_3, with w_4 as an auxiliary vertex.

4. Negation handling: For negated literals, swap the connection: connect to the f_i node instead of the t_i node (or equivalently, cross the wires in the equality gadget).

Output: Graph G is the union of all gadgets with their interconnecting edges, K = 2.

Correctness sketch:

• If the NAE-3SAT instance is satisfiable (with a not-all-equal assignment), assign colors to variable pairs according to truth values. The clause gadgets can then be consistently 2-colored because the NAE condition ensures not all three literals in any clause are the same, which is exactly what the K_4 gadget requires.
• Conversely, if G admits a 2-colorable perfect matching, the color assignment to variable pairs gives a truth assignment, and the K_4 clause gadgets ensure the NAE condition holds for every clause.

Note: The precise gadget wiring follows Schaefer's 1978 construction. The above is a high-level summary; the exact vertex counts depend on the specific equality gadget used.

Size Overhead

Symbols:

• n = num_variables of source NAE-3SAT instance
• m = num_clauses of source NAE-3SAT instance
• L = total number of literal occurrences (at most 3m)

Target metric (code name)	Polynomial (using symbols above)
num_vertices	O(n + m) -- exact constant depends on gadget sizes
num_edges	O(n + m) -- each gadget has constant-size edge set
num_matchings	2 (always)

Derivation: Each variable contributes a constant number of vertices (variable pair plus copies for each occurrence). Each clause contributes a K_4 gadget (4 vertices, 6 edges). Equality gadgets add a constant number of vertices per variable occurrence. The total is linear in n + L = O(n + m).

Validation Method

• Closed-loop test: reduce a NAESatisfiability instance to PartitionIntoPerfectMatchings, solve the target with BruteForce (enumerate all 2-colorings of vertices, check each vertex has exactly one same-color neighbor), extract the coloring, map back to truth assignment, verify the NAE condition holds for every clause.
• Test with known satisfiable and unsatisfiable NAE-3SAT instances.
• Verify small cases: a single clause (x, y, z) with 3 variables should produce a small graph where 2-coloring exists iff the clause is NAE-satisfiable (which it always is for a single clause with distinct variables).

Example

Source instance (NAESatisfiability):
NAE-3SAT with 3 variables {x_1, x_2, x_3} and 1 clause:

• Clause: (x_1, x_2, x_3)
• This is NAE-satisfiable: e.g., x_1 = TRUE, x_2 = TRUE, x_3 = FALSE satisfies NAE (not all equal).
• Also x_1 = FALSE, x_2 = FALSE, x_3 = TRUE works (complement).

Constructed target instance (PartitionIntoPerfectMatchings):
The reduction produces a graph G with K = 2. The exact graph depends on the gadget construction:

• Variable gadget for x_1: vertices {t_1, f_1}, edge {t_1, f_1}
• Variable gadget for x_2: vertices {t_2, f_2}, edge {t_2, f_2}
• Variable gadget for x_3: vertices {t_3, f_3}, edge {t_3, f_3}
• Clause gadget (K_4): vertices {w_1, w_2, w_3, w_4}, edges: all 6 edges of K_4
• Interconnection edges linking t_1 to w_1, t_2 to w_2, t_3 to w_3 (for positive literals)
• Total: 10 vertices, ~12 edges (exact count depends on equality gadget details)

Solution mapping:

• A valid 2-coloring of G where each vertex has exactly one same-color neighbor encodes:
  • Color of (t_1, f_1) pair -> truth value of x_1
  • Color of (t_2, f_2) pair -> truth value of x_2
  • Color of (t_3, f_3) pair -> truth value of x_3
• The K_4 clause gadget ensures not all three literals get the same color, enforcing NAE.

Note: The exact graph structure requires implementing Schaefer's specific gadget construction. The above is schematic.

References

• [Schaefer, 1978b]: [Schaefer1978b] T. J. Schaefer (1978). "The complexity of satisfiability problems". In: Proceedings of the 10th Annual ACM Symposium on Theory of Computing, pp. 216–226. Association for Computing Machinery.

[GiggleLiu]

Implemented in PR #1010.