[Rule] KSatisfiability to MaxCut

[zazabap]

Source: NAESatisfiability
Target: MaxCut
Motivation: Classic NP-completeness reduction connecting Boolean satisfiability to graph partitioning. The Not-All-Equal structure is the key: every satisfied NAE clause contributes exactly 2 triangle edges to the cut, while every unsatisfied clause (all literals equal) contributes 0. This clean characterization establishes MaxCut as NP-hard via NAE-3SAT.
Reference: Garey, Johnson & Stockmeyer, "Some simplified NP-complete graph problems," Theoretical Computer Science 1(3), 237–267 (1976). Also: Garey & Johnson, Computers and Intractability (1979), Section 3.2.5.

Reduction Algorithm

Given a NAE-3SAT instance with $n$ variables $x_1, \ldots, x_n$ and $m$ clauses $C_1, \ldots, C_m$ (each clause has exactly 3 literals; for each clause, not all literals may be simultaneously true and not all simultaneously false):

Notation:

• $n$ = num_vars, $m$ = num_clauses
• For variable $x_i$, create two vertices: $v_i$ (positive literal) and $v_i'$ (negative literal)
• Forcing weight $M = 2m + 1$

Variable gadgets:

1. For each variable $x_i$, create vertices $v_i$ and $v_i'$.
2. Add edge $(v_i, v_i')$ with weight $M$.

Since $M = 2m+1 > 2m$ equals the maximum possible total clause contribution (at most 2 per clause), the optimal cut always cuts every variable-gadget edge. This forces $v_i$ and $v_i'$ to opposite sides. The side containing $v_i$ encodes $x_i = \text{true}$.

Clause gadgets:
3. For each clause $C_j = (\ell_a, \ell_b, \ell_c)$:

• Add a triangle of weight-1 edges: $(\ell_a, \ell_b)$, $(\ell_b, \ell_c)$, $(\ell_a, \ell_c)$.

Why NAE is essential:
For a NAE clause, the induced partition has 1 literal on one side and 2 on the other (or vice versa). A triangle with exactly $1+2$ split has exactly 2 edges crossing the cut. A triangle with all 3 on the same side contributes 0 — but the NAE constraint forbids this. Without NAE (standard 3-SAT), a clause with all literals true places all 3 literal-vertices on the same side, contributing 0 — identical to the unsatisfied case. The triangle gadget cannot distinguish the two, breaking the reduction. NAE exactly avoids this degenerate case.

Cut threshold:
4. The instance is NAE-satisfiable if and only if the maximum weighted cut $\geq n \cdot M + 2m$.

• Satisfiable: every clause contributes exactly 2 → total = $nM + 2m$.
• Unsatisfiable: every truth assignment has at least one clause with all literals equal (contributing 0) → total clause contribution $\leq 2(m-1)$ → cut $\leq nM + 2m - 2 < nM + 2m$.

Solution extraction: For variable $x_i$, if $v_i \in S$, set $x_i = \text{true}$; otherwise $\text{false}$.

Size Overhead

Target metric (code name)	Formula
num_vertices	$2n$ = 2 * num_vars
num_edges	$n + 3m$ = num_vars + 3 * num_clauses

(Clause triangle edges connect literal-vertices of distinct variables within a clause; they are distinct from variable-gadget edges, which connect $v_i$ to $v_i'$. If a triangle edge happens to connect a complementary pair from the same variable — only possible when a clause contains both $x_i$ and $\neg x_i$ — that edge coincides with a variable-gadget edge and its weight accumulates. The formula num_vars + 3 * num_clauses is therefore a worst-case upper bound on distinct edges.)

Validation Method

• Construct small NAE-3SAT instances where no clause contains both $x_i$ and $\neg x_i$ (so no edge merging occurs), reduce to MaxCut, solve both with BruteForce.
• Verify: satisfying assignment maps to cut $= nM + 2m$.
• Verify: unsatisfiable instance has maximum cut $< nM + 2m$.
• Test both satisfiable (e.g., a colorable graph encoded as NAE-3SAT) and unsatisfiable instances.

Example

Source: NAE-3SAT with $n=3$, $m=2$, $M = 2(2)+1 = 5$

• Variables: $x_1, x_2, x_3$
• $C_1 = (x_1, x_2, x_3)$ (NAE: not all equal)
• $C_2 = (\neg x_1, \neg x_2, \neg x_3)$ (NAE: not all equal)

Reduction:

• Vertices: $v_1, v_1', v_2, v_2', v_3, v_3'$ (6 = $2n$ ✓)
• Variable-gadget edges: $(v_1,v_1')$ w=5, $(v_2,v_2')$ w=5, $(v_3,v_3')$ w=5
• $C_1$ triangle: $(v_1,v_2)$ w=1, $(v_2,v_3)$ w=1, $(v_1,v_3)$ w=1
• $C_2$ triangle: $(v_1',v_2')$ w=1, $(v_2',v_3')$ w=1, $(v_1',v_3')$ w=1
• Total edges: 9 = $n + 3m = 3 + 6$ ✓ (no merges — clause edges connect distinct-variable literal pairs)

Satisfying assignment: $x_1=T, x_2=F, x_3=F$

• Partition: $S={v_1, v_2', v_3'}$, $\bar S={v_1', v_2, v_3}$
• Variable-gadget cut: all 3 edges cross → $3 \times 5 = 15$
• $C_1$ triangle: $(v_1, v_2)$ crosses ($v_1\in S, v_2\in\bar S$), $(v_1,v_3)$ crosses ($v_1\in S, v_3\in\bar S$), $(v_2,v_3)$ does not ($v_2,v_3\in\bar S$) → 2 edges cut ✓
• $C_2$ triangle: $(v_1',v_2')$ crosses ($v_1'\in\bar S, v_2'\in S$), $(v_1',v_3')$ crosses ($v_1'\in\bar S, v_3'\in S$), $(v_2',v_3')$ does not ($v_2',v_3'\in S$) → 2 edges cut ✓
• Total cut = 15 + 2 + 2 = 19
• Threshold = $nM + 2m = 3(5) + 2(2) = 19$ ✓

Unsatisfying assignment: $x_1=T, x_2=T, x_3=T$ (fails $C_1$: all true)

• Partition: $S={v_1,v_2,v_3}$, $\bar S={v_1',v_2',v_3'}$
• Variable-gadget cut: $15$
• $C_1$ triangle: all of $v_1,v_2,v_3\in S$ → 0 edges cut
• $C_2$ triangle: all of $v_1',v_2',v_3'\in\bar S$ → 0 edges cut
• Total cut = 15 < 19 = threshold ✓

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	⚠️ Warn	Existing 4-step path (KSat->SAT->CircuitSAT->SpinGlass->MaxCut) has overhead num_vertices = num_clauses + 2; proposed direct path uses 2n vertices — not strictly better
Non-trivial	✅ Pass	Genuine structural transformation with variable gadgets and clause triangle gadgets
Correctness	❌ Fail	Threshold formula and edge count appear incorrect; construction details deviate from standard literature
Well-written	❌ Fail	Edge count formula inconsistent; symbol definitions have gaps; example incomplete

Overall: 1 passed, 1 warning, 2 failed

---

Usefulness

An existing 4-step path already connects KSatisfiability to MaxCut:

KSatisfiability -> Satisfiability -> CircuitSAT -> SpinGlass -> MaxCut

The composed overhead of this path is num_vertices = num_clauses + 2, num_edges = num_clauses + 2, which depends only on m (number of clauses) and produces a very compact MaxCut instance.

The proposed direct reduction creates num_vertices = 2n and num_edges = n + 6m (as claimed). Since the existing path overhead is linear in m only and the proposed is linear in both n and m, the overhead comparison is ambiguous — neither strictly dominates the other. However, a direct single-step reduction has value for simplicity and pedagogical clarity. The Motivation field is adequate but could be stronger about why a direct path is preferable to the existing 4-step chain.

Non-trivial

The reduction involves genuine structural transformation: variable gadgets (pairs of complement vertices connected by weighted edges) and clause gadgets (triangles connecting literal-vertices with complement edges). This is a well-known construction pattern in NP-completeness theory. Pass.

Correctness

The issue cites two references:

1. Garey, Johnson & Stockmeyer (1976), "Some simplified NP-complete graph problems," TCS 1(3), 237-267. — This paper exists (DOI: 10.1016/0304-3975(76)90059-1) and does establish MaxCut NP-completeness. However, this paper focuses on showing problems remain NP-complete under domain restrictions (e.g., planar graphs, bounded degree), not on the specific 3-SAT-to-MaxCut gadget construction described in the issue.

2. Garey & Johnson (1979), Computers and Intractability, Section 3.2.5. — The book exists and lists MaxCut as problem GT24. It catalogs the reduction but the specific construction details in the issue need verification.

Technical issues with the proposed construction:

(a) Threshold formula appears incorrect. The issue claims the cut threshold is n * m + 2m. However, the construction adds complement edges (weight 1 each) to the variable-gadget edges for each clause. With m clauses of 3 literals each, the variable-gadget edges accumulate a total of 3m additional weight from complement edges on top of the base n * m. So cutting all variable-gadget edges contributes n*m + 3m (not n*m), and the clause triangles contribute up to 2m from satisfied clauses. The threshold should be n*m + 3m + 2m = n*m + 5m, not n*m + 2m. The standard construction in the literature (e.g., Cornell CS 4820 notes by David Steurer) uses variable edge capacity M = 10*m specifically to ensure a gap large enough to force variable-complement separation, with threshold n*10m + 2m.

(b) The base weight m may be insufficient. If a variable-gadget edge is NOT cut (both endpoints on same side), we lose weight m + occurrences from that edge. The maximum gain from clause triangles is 3m (if all 3 edges of every clause triangle are cut). With base weight m, the gap between cutting vs. not cutting a variable edge is too small to force consistent truth assignment. The standard construction uses M = 10*m or similar large multiple to ensure this forcing property.

(c) Edge count formula is internally inconsistent. The issue claims num_edges = n + 6m, described as "variable-gadget base edges + 3 triangle edges + 3 complement edges per clause; parallel edges merged by summing weights." But if parallel edges are merged, the complement edges (which go between v_i and v_i', the same pairs as variable-gadget edges) do NOT create new distinct edges — they increase weights on existing edges. After merging, the distinct edge count is n + 3m (n variable-gadget edges + 3m clause triangle edges), not n + 6m.

Well-written

4a — Information Completeness: All template sections (Source, Target, Motivation, Reference, Reduction Algorithm, Size Overhead, Validation Method, Example) are present and substantive. Pass on template structure.

4b — Algorithm Completeness: The algorithm is a step-by-step procedure that a programmer could follow. However, Step 4 (cut threshold) mixes the construction description with the correctness argument in a way that obscures the actual threshold value. The solution extraction step is brief but adequate.

4c — Symbol and Notation Consistency:

• The symbol n is defined as "number of variables" and m as "number of clauses" — good.
• The overhead table uses code metric names num_vertices and num_edges, which match MaxCut's actual size fields — good.
• However, the edge count formula n + 6m is inconsistent with the algorithm description that says "parallel edges merged by summing weights." After merging, there are only n + 3m distinct edges. Fail.

4d — Example Quality:

• The example uses n=3, m=2, which is reasonable in size.
• The variable edge weights are computed correctly (base 2 + 1 + 1 = 4 each).
• However, the example does not compute the final cut value or verify the threshold formula. It says "The cut crosses all variable-gadget edges (contributing 12) plus clause triangle edges that span the partition" but does not enumerate which triangle edges are cut or compute the total cut value. This makes the example incomplete — it should be fully worked to verify the threshold claim. Fail.

Recommendations

• The standard reduction from 3-SAT to MaxCut in the literature typically goes through NAE-3-SAT (Not-All-Equal 3-SAT), not directly. Consider using the NAE-3-SAT route: 3-SAT -> NAE-4-SAT -> NAE-3-SAT -> MaxCut. Alternatively, if a direct construction is intended, use the version with variable edge weight M = 10*m (or similar sufficiently large value) as in Steurer's Cornell CS 4820 notes.
• Fix the edge count to n + 3m after parallel edge merging, or if the intent is to NOT merge parallel edges, clarify that the target graph uses a multigraph representation.
• Complete the example by computing the exact cut value for the given partition and verifying it against the threshold formula.
• Correct the threshold formula to account for the complement edge weights accumulated on the variable-gadget edges.

[zazabap]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Direct 1-step reduction vs existing 4-step path (KSat → SAT → CircuitSAT → SpinGlass → MaxCut)
Non-trivial	✅ Pass	Gadget construction with variable-complement edges and clause triangles
Correctness	⚠️ Warn	Reference is valid but cited as the source of this specific construction; see details below
Well-written	❌ Fail	Edge count formula contradicts "parallel edges merged"; example incomplete

Overall: 2 passed, 1 warning, 1 failed

---

Usefulness

The existing path from KSatisfiability to MaxCut requires 4 hops through Satisfiability → CircuitSAT → SpinGlass → MaxCut, with overall overhead num_vertices = num_clauses + 2, num_edges = num_clauses + 2. The proposed reduction is a direct 1-step reduction with overhead expressed in terms of both num_vars and num_clauses. While the overhead expressions are not directly comparable (different variables), a direct single-step reduction is valuable for clarity and avoids accumulated imprecision from chaining 4 reductions. Pass.

Non-trivial

The reduction constructs variable gadgets (complementary literal pairs with high-weight edges) and clause gadgets (triangles connecting literal vertices), with additional complement edges accumulating weights. This involves genuine structural transformation — not a relabeling or type coercion. Pass.

Correctness

Reference verification:

• Garey, Johnson & Stockmeyer, "Some simplified NP-complete graph problems," Theoretical Computer Science 1(3), 237–267 (1976) — Verified. The paper exists with matching authors, title, journal, volume, and DOI (10.1016/0304-3975(76)90059-1). It is already partially in the project bibliography as garey1979 (the textbook).
• Garey & Johnson, Computers and Intractability (1979), Section 3.2.5 — Verified. Known textbook, already in references.bib.

Claim accuracy concern: The Garey-Johnson-Stockmeyer (1976) paper proves MaxCut NP-completeness via a reduction from NAE-3SAT (Not-All-Equal 3-SAT) to MaxCut, not directly from 3-SAT. The construction described in this issue (variable edges with weight m, clause triangles with complement edges, threshold n*m + 2m) corresponds to the direct 3-SAT → MaxCut reduction found in textbook presentations (e.g., David Steurer, Cornell CS 4820, 2014), which is a standard pedagogical variant. The issue should clarify which construction it follows — if it intends the GJS construction, the description is inaccurate (GJS goes through NAE-SAT); if it intends the direct textbook reduction, a more specific citation would be appropriate.

Construction correctness: The described variable gadget (weight m edges forcing complements to opposite sides) and clause triangle construction are consistent with known direct 3-SAT → MaxCut reductions. The threshold n*m + 2m is correct for this variant. Warn due to citation-construction mismatch.

Well-written

4a — Information Completeness: All required sections are present. ✅

4b — Algorithm Completeness: The step-by-step procedure is detailed enough to implement. ✅

4c — Symbol and Notation Consistency:

Edge count formula is internally contradictory. The Size Overhead table states:

num_edges = n + 6m (variable-gadget base edges + 3 triangle edges + 3 complement edges per clause; parallel edges merged by summing weights)

This counts 6 edges per clause (3 triangle + 3 complement). But the description also says "parallel edges merged by summing weights." The complement edges connect each literal to its complement — the same vertex pair as the variable-gadget edges. After merging, they do not create new edges; they only increase the weight of existing variable-gadget edges. The correct count after merging should be:

num_edges = n + 3m (at most — n variable-gadget edges + up to 3m triangle edges, some of which may also overlap between clauses)

In the worked example: 3 variable edges + 6 triangle edges = 9 distinct edges, while the formula gives 3 + 6*2 = 15. This confirms the formula is wrong. ❌

4c — Size field names: The target is MaxCut, whose size_fields are num_vertices and num_edges. The overhead table uses these correctly. ✅

4d — Example Quality:

The example is non-trivial (3 variables, 2 clauses) and the construction is shown step-by-step. However:

• The final cut value is not computed. The issue says "the cut crosses all variable-gadget edges (contributing 12) plus clause triangle edges that span the partition" but does not give the total cut value or verify it against the threshold n*m + 2m = 3*2 + 2*2 = 10. Without completing this calculation, the example does not fully demonstrate correctness. ❌
• The specific triangle edges crossing the partition are not enumerated, so the reader cannot verify the example by hand.

Summary of failures:

1. num_edges overhead formula counts merged parallel edges as distinct — should be n + 3m, not n + 6m
2. Example does not compute the final cut value or verify it against the threshold

Recommendations

• Fix the edge count formula to n + 3m (after merging parallel edges) or, if the intent is to keep parallel edges separate (multigraph), remove the "parallel edges merged" note and clarify that MaxCut here operates on a multigraph
• Complete the example by computing the total cut value and verifying it equals or exceeds the threshold n*m + 2m
• Clarify the citation: if using the direct 3-SAT → MaxCut construction (not the NAE-3SAT route from GJS 1976), cite a textbook presentation that gives this specific construction, or note that it is a standard adaptation of the GJS technique

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Direct 1-step reduction vs existing 4-step path; not dominated
Non-trivial	✅ Pass	Genuine gadget construction with variable/clause gadgets
Correctness	❌ Fail	Threshold formula wrong; variable edge weight too small; reference mismatch
Well-written	❌ Fail	Edge count contradicts "parallel edges merged"; example incomplete

Overall: 2 passed, 0 warnings, 2 failed

---

Usefulness

Existing 4-step path: KSatisfiability → Satisfiability → CircuitSAT → SpinGlass → MaxCut with composed overhead num_vertices = num_clauses + 2, num_edges = num_clauses + 2. The proposed direct reduction uses num_vertices = 2n, num_edges = n + 3m (corrected). Since the existing path depends only on m and the proposed depends on both n and m, neither strictly dominates. A direct 1-step reduction is still valuable for simplicity. Pass.

Non-trivial

The reduction involves genuine structural transformation: variable gadgets (complement vertex pairs with weighted edges) and clause gadgets (triangles with complement edges). Not a relabeling or type coercion. Pass.

Correctness

Reference verification:

• Garey, Johnson & Stockmeyer (1976), TCS 1(3), 237–267 — Exists (already in references.bib). However, this paper proves MaxCut NP-completeness via NAE-3SAT, not a direct 3-SAT→MaxCut construction. The specific gadget in this issue (variable edges weight m, clause triangles + complement edges, threshold n*m + 2m) does not come from this paper.
• Garey & Johnson (1979), Section 3.2.5 — Exists (already in references.bib). Lists MaxCut as GT24, but the construction here does not match the standard textbook reduction chain (which goes through NAE-3SAT).

Threshold formula is incorrect — verified by brute-force enumeration:

Python script reproducing the issue's example (n=3, m=2, C1=(x1∨x2∨x3), C2=(¬x1∨¬x2∨x3)) found:

Assignment	Satisfying?	Cut value
x1=F, x2=T, x3=F	Yes	16
x1=F, x2=T, x3=T	Yes	16
x1=T, x2=F, x3=F	Yes	16
x1=T, x2=F, x3=T	Yes	16
x1=F, x2=F, x3=T	Yes	14
x1=T, x2=T, x3=T	Yes	14
x1=F, x2=F, x3=F	No	14
x1=T, x2=T, x3=F	No	14

The claimed threshold is n*m + 2m = 10. Both unsatisfying assignments produce cuts of 14, which is above the threshold. The threshold fails to discriminate satisfying from unsatisfying assignments.

Root cause: The variable edge base weight m = 2 is too small to force the complementary-side property. MaxCut is symmetric under partition complementation (flipping all sides), but 3-SAT is not. With weight m, the gap between cutting and not cutting a variable edge is only m + occurrences ≈ 4, while clause triangles contribute up to 6 total. The standard construction uses M = 10m (or similar large multiple) to ensure this forcing property works.

The correct approach is either:

1. Use the standard route: 3-SAT → NAE-3SAT → MaxCut (which exploits the fact that NAE-SAT shares MaxCut's complementation symmetry)
2. Use variable edge weight M ≫ m (e.g., M = 10m) as in Steurer's Cornell CS 4820 notes, which provides sufficient gap to force variable-complement separation

❌ Fail — the construction does not correctly reduce 3-SAT to MaxCut.

Well-written

4a — Required sections: All present. ✅

4b — Algorithm completeness: Steps are numbered and follow-able, but Step 4 mixes construction with correctness argument. ⚠️

4c — Symbol and notation consistency:

The Size Overhead table states num_edges = n + 6m described as "variable-gadget base edges + 3 triangle edges + 3 complement edges per clause; parallel edges merged by summing weights." This is self-contradictory: the complement edges connect (v_i, v_i') — the same pairs as variable-gadget edges. After merging parallel edges, complement edges do not create new distinct edges. The correct count after merging is n + 3m (n variable edges + 3m triangle edges). In the worked example: 3 variable edges + 6 triangle edges = 9 distinct edges, while the formula gives 3 + 6*2 = 15. ❌ Fail.

4d — Example quality:

The example is non-trivial (n=3, m=2) and construction steps are shown. However:

1. The final cut value is never computed — the issue says "the cut crosses all variable-gadget edges (contributing 12) plus clause triangle edges that span the partition" without enumerating which triangle edges cross or giving the total. Not fully worked. ❌
2. The threshold is not verified against the example. ❌
3. Brute-force verification (above) shows the threshold is wrong, so even if completed the example would expose the bug. ❌

❌ Fail — edge count formula wrong, example incomplete.

Recommendations

1. Fix the construction. Either:
   • Switch to NAE-3SAT → MaxCut (standard, simpler, correct)
   • Use variable edge weight M = 10m for a direct 3-SAT → MaxCut construction and rederive the threshold
2. Fix the edge count to n + 3m after merging, or clarify multigraph intent
3. Fix the reference — cite the actual source of the specific construction used (e.g., Steurer's CS 4820 notes for the direct construction, or GJS 1976 for the NAE-3SAT route)
4. Complete the example — compute exact cut value, enumerate crossing edges, verify against (corrected) threshold

[isPANN]

Maintainer Recommendation

The construction is fundamentally broken, not just a weight issue

After deeper analysis, the triangle clause gadget cannot work for ordinary 3-SAT → MaxCut with any variable edge weight M. The issue is not just that M=m is too small — even M=10m fails.

Root cause: The triangle gadget treats "all 3 literals true" (satisfied in 3-SAT) identically to "all 3 literals false" (unsatisfied). Both contribute 0 edges to the cut:

Clause true literals	Satisfied?	Triangle cut edges
3 (all true)	✅ Yes	0 (all vertices same side)
2	✅ Yes	2
1	✅ Yes	2
0 (all false)	❌ No	0 (all vertices same side)

This means a satisfying assignment where every clause has all-3-true gives cut = nM + 0, while an unsatisfying assignment with only one bad clause gives cut = nM + 2(m−1). The satisfying assignment has a lower cut value — the reduction breaks.

The complement edges don't help: they merge into variable edges and contribute the same amount regardless of truth assignment.

Why NAE-3SAT works

NAE-3SAT (Not-All-Equal) requires at least one true AND at least one false literal per clause, which excludes the "all true" case. This matches MaxCut's complementation symmetry perfectly — every satisfied NAE clause contributes exactly 2 triangle edges to the cut.

Recommendation

Close this issue and replace with the proper reduction chain if desired:

1. [Model] NotAllEqualSatisfiability — NAE-k-SAT problem
2. [Rule] KSatisfiability → NotAllEqualSatisfiability — standard reduction using auxiliary variable per clause
3. [Rule] NotAllEqualSatisfiability → MaxCut — triangle gadget with M=10m (this is the construction the issue was trying to describe, but it only works for NAE-SAT)

Alternatively, a direct 3-SAT → MaxCut construction exists using different clause gadgets (auxiliary vertices per clause, not simple triangles), but it is significantly more complex and less standard.