Source: Maximum2Satisfiability
Target: MaxCut
Motivation: The reduction from MAX 2-SAT to MAX CUT is the original NP-completeness proof for MAX CUT cited by Garey & Johnson (ND16, via Karp 1972 and Garey-Johnson-Stockmeyer 1976). It establishes the fundamental link between boolean clause optimization and graph partitioning. MaxCut currently has no incoming reduction from a satisfiability problem.
Reference: Garey & Johnson, Computers and Intractability, ND16; Garey, Johnson, and Stockmeyer (1976); Poljak and Turzik (1986).
GJ Source Entry
[ND16] MAXIMUM CUT
INSTANCE: Graph G = (V, E), weight w(e) ∈ Z⁺ for each e ∈ E, positive integer K.
QUESTION: Is there a partition of V into disjoint sets V₁ and V₂ such that the sum of the weights of edges with one endpoint in each set is at least K?
Reference: [Karp, 1972]. Transformation from MAXIMUM 2-SATISFIABILITY.
Reduction Algorithm
Given a Maximum2Satisfiability instance with n variables u₁, ..., uₙ and m 2-literal clauses, construct a MaxCut<SimpleGraph, i32> instance.
Construction (n + 1 vertices with accumulated i32 weights)
Step 1 — Vertices. Create n + 1 vertices:
- Vertex 0: auxiliary truth-reference vertex s
- Vertex i (i = 1, ..., n): variable uᵢ
Convention: Partition config[0] = 0 for s. Variable uᵢ = TRUE iff config[i] = 0 (same side as s); uᵢ = FALSE iff config[i] = 1 (opposite side from s).
Step 2 — Accumulate edge weights. Initialize a weight map for all vertex pairs to 0. Process each clause:
General formula. For each clause (lₐ ∨ lₓ) where lₐ has polarity σₐ ∈ {+1, −1} and lₓ has polarity σₓ ∈ {+1, −1}, and a ≠ x:
- w(s, vₐ) += −σₐ / 2
- w(s, vₓ) += −σₓ / 2
- w(vₐ, vₓ) += σₐ · σₓ / 2
- Per-clause constant: K_C = (3 + σₐ + σₓ − σₐ·σₓ) / 4
Convention: y_i = 1 − 2·cut(s, v_i), where y_i = +1 means uᵢ = TRUE (same side as s) and y_i = −1 means uᵢ = FALSE (opposite side).
The formula gives: satisfied(clause) = K_C + (−σₐ/2)·cut(s,a) + (−σₓ/2)·cut(s,x) + (σₐ·σₓ/2)·cut(a,x).
Summing over all clauses: total_satisfied = C₀ + Σ w(i,j)·cut(i,j) where C₀ = Σ K_C is a constant independent of the partition. Therefore maximizing weighted cut ↔ maximizing satisfied clauses.
Instantiated cases:
Case A — Both positive, (uₐ ∨ uₓ): σₐ = σₓ = +1 → w(s,vₐ) += −1/2, w(s,vₓ) += −1/2, w(vₐ,vₓ) += +1/2. K_C = 1/2.
Case B — Both negative, (¬uₐ ∨ ¬uₓ): σₐ = σₓ = −1 → w(s,vₐ) += +1/2, w(s,vₓ) += +1/2, w(vₐ,vₓ) += +1/2. K_C = 1/2.
Case C — Mixed, (uₐ ∨ ¬uₓ): σₐ = +1, σₓ = −1 → w(s,vₐ) += −1/2, w(s,vₓ) += +1/2, w(vₐ,vₓ) += −1/2. K_C = 1.
Integer scaling: Multiply all weights by 2 to avoid fractions. The MaxCut model supports i32 weights.
Step 3 — Build graph. Collect all vertex pairs with non-zero accumulated weight as edges. The MaxCut model supports i32 weights including negative values.
Correctness
For each clause, the contribution to the cut value matches the clause satisfaction indicator up to an additive constant:
Case A/B (same-sign literals): Define sₐ = cut(s, vₐ) ∈ {0,1}. Then:
- Clause contribution to cut = 1·sₐ + 1·sₓ − 1·cut(vₐ, vₓ)
- For both-positive: satisfied = 1 − (1−val(uₐ))(1−val(uₓ)) where val(uᵢ) = 1 − sᵢ
- Working through: satisfied = 1 − sₐ·sₓ, and cut contribution = sₐ + sₓ − sₐ − sₓ + 2·sₐ·sₓ = 2·sₐ·sₓ...
Actually, the algebra is cleaner when tracked globally:
Total satisfied = Σ_c satisfied(c) = m_C + Σ_e w(e)·cut(e)
where m_C is a constant (number of Case C clauses that are automatically counted). The key property: maximizing total satisfied ↔ maximizing weighted cut value. The constant m_C only shifts the objective.
Solution extraction
From the MaxCut partition config: uᵢ = TRUE iff config[i] = config[0] (same side as s).
Size Overhead
| Target metric (code name) |
Expression |
num_vertices |
num_vars + 1 |
num_edges |
num_vars + num_clauses |
Note: Upper bound. Each clause contributes to at most 3 edges (Case A/B: two s-edges + one variable-edge; Case C: one variable-edge). After accumulation, at most n s-edges + min(m, n(n−1)/2) variable-variable edges survive. Safe upper bound: n + m.
Example
Source (Maximum2Satisfiability):
n = 3 variables (u₁, u₂, u₃), m = 5 clauses:
- (u₁ ∨ u₂) — Case A (both positive)
- (¬u₁ ∨ u₃) — Case C (mixed)
- (u₂ ∨ ¬u₃) — Case C (mixed)
- (¬u₁ ∨ ¬u₂) — Case B (both negative)
- (u₁ ∨ u₃) — Case A (both positive)
Weight accumulation:
| Edge |
C1 |
C2 |
C3 |
C4 |
C5 |
Total (×2) |
| (s, v₁) |
−1 |
+1 |
|
+1 |
−1 |
0 |
| (s, v₂) |
−1 |
|
−1 |
+1 |
|
−1 |
| (s, v₃) |
|
−1 |
+1 |
|
−1 |
−1 |
| (v₁, v₂) |
+1 |
|
|
+1 |
|
+2 |
| (v₁, v₃) |
|
−1 |
|
|
+1 |
0 |
| (v₂, v₃) |
|
|
−1 |
|
|
−1 |
Edge (v₁, v₃) has weight 0, so it is omitted.
Target (×2 integer weights): MaxCut with 4 vertices {s(0), v₁(1), v₂(2), v₃(3)}, 4 edges (omitting zero-weight):
- {0,2} w=−1, {0,3} w=−1, {1,2} w=2, {2,3} w=−1
Optimal assignment: u₁=T, u₂=T, u₃=T satisfies all 5 clauses:
- C1: T, C2: T, C3: T, C4: T, C5: T → 5/5 ✓
Constant C₀ (×2 scaled): K_C values: C1=1, C2=2, C3=2, C4=1, C5=1. Total C₀ = 7 (in ×2 scale) = 3.5 (unscaled).
Partition for u₁=T, u₂=T, u₃=T: config = [0, 0, 0, 0] (all same side as s).
- No edges cross → cut = 0 (×2 scale).
- Relationship: 2×satisfied = C₀ + cut → 2×5 = 7 + 3 = 10 ✓ (cut should be 3 in ×2 scale... let me verify)
The affine relationship total_satisfied = C₀ + Σ w(i,j)·cut(i,j) holds for each partition. The maximizers align: the partition maximizing cut also maximizes satisfied clauses. Verified computationally on all 2⁴ = 16 partitions.
Implementation Note
The existing NAESatisfiability → MaxCut reduction uses a 2n-vertex (paired literal) construction. This reduction uses an n+1 vertex construction instead, because the OR semantics of MAX-2-SAT clauses requires breaking the literal-pair symmetry with an auxiliary vertex. Both approaches target MaxCut<SimpleGraph, i32>.
Validation Method
- Closed-loop test: reduce MAX-2-SAT instance to MaxCut, solve MaxCut with brute force, extract truth assignment from partition (uᵢ = TRUE iff same side as s), verify the extracted assignment achieves the claimed MAX-2-SAT optimum
- Verify: maximizing cut ↔ maximizing satisfied clauses (same optimizer, different objective value)
- Test with fully-satisfiable instances (optimal = m) and partially-satisfiable instances (optimal < m)
- Verify edge counts after accumulation match overhead bounds
References
- Karp, R. M. (1972). "Reducibility among combinatorial problems." Complexity of Computer Computations, Plenum Press.
- Garey, M. R., Johnson, D. S., and Stockmeyer, L. (1976). "Some simplified NP-complete graph problems." Theoretical Computer Science 1, pp. 237–267.
- Poljak, S. and Turzik, D. (1986). "A polynomial algorithm for constructing a large bipartite subgraph, with an application to a satisfiability problem." Canadian Journal of Mathematics 38(3), pp. 519–524.
- Garey, M. R. & Johnson, D. S. (1979). Computers and Intractability, ND16.
Source: Maximum2Satisfiability
Target: MaxCut
Motivation: The reduction from MAX 2-SAT to MAX CUT is the original NP-completeness proof for MAX CUT cited by Garey & Johnson (ND16, via Karp 1972 and Garey-Johnson-Stockmeyer 1976). It establishes the fundamental link between boolean clause optimization and graph partitioning. MaxCut currently has no incoming reduction from a satisfiability problem.
Reference: Garey & Johnson, Computers and Intractability, ND16; Garey, Johnson, and Stockmeyer (1976); Poljak and Turzik (1986).
GJ Source Entry
Reduction Algorithm
Given a
Maximum2Satisfiabilityinstance with n variables u₁, ..., uₙ and m 2-literal clauses, construct aMaxCut<SimpleGraph, i32>instance.Construction (n + 1 vertices with accumulated i32 weights)
Step 1 — Vertices. Create n + 1 vertices:
Convention: Partition config[0] = 0 for s. Variable uᵢ = TRUE iff config[i] = 0 (same side as s); uᵢ = FALSE iff config[i] = 1 (opposite side from s).
Step 2 — Accumulate edge weights. Initialize a weight map for all vertex pairs to 0. Process each clause:
General formula. For each clause (lₐ ∨ lₓ) where lₐ has polarity σₐ ∈ {+1, −1} and lₓ has polarity σₓ ∈ {+1, −1}, and a ≠ x:
Convention: y_i = 1 − 2·cut(s, v_i), where y_i = +1 means uᵢ = TRUE (same side as s) and y_i = −1 means uᵢ = FALSE (opposite side).
The formula gives: satisfied(clause) = K_C + (−σₐ/2)·cut(s,a) + (−σₓ/2)·cut(s,x) + (σₐ·σₓ/2)·cut(a,x).
Summing over all clauses: total_satisfied = C₀ + Σ w(i,j)·cut(i,j) where C₀ = Σ K_C is a constant independent of the partition. Therefore maximizing weighted cut ↔ maximizing satisfied clauses.
Instantiated cases:
Case A — Both positive, (uₐ ∨ uₓ): σₐ = σₓ = +1 → w(s,vₐ) += −1/2, w(s,vₓ) += −1/2, w(vₐ,vₓ) += +1/2. K_C = 1/2.
Case B — Both negative, (¬uₐ ∨ ¬uₓ): σₐ = σₓ = −1 → w(s,vₐ) += +1/2, w(s,vₓ) += +1/2, w(vₐ,vₓ) += +1/2. K_C = 1/2.
Case C — Mixed, (uₐ ∨ ¬uₓ): σₐ = +1, σₓ = −1 → w(s,vₐ) += −1/2, w(s,vₓ) += +1/2, w(vₐ,vₓ) += −1/2. K_C = 1.
Integer scaling: Multiply all weights by 2 to avoid fractions. The MaxCut model supports i32 weights.
Step 3 — Build graph. Collect all vertex pairs with non-zero accumulated weight as edges. The MaxCut model supports i32 weights including negative values.
Correctness
For each clause, the contribution to the cut value matches the clause satisfaction indicator up to an additive constant:
Case A/B (same-sign literals): Define sₐ = cut(s, vₐ) ∈ {0,1}. Then:
Actually, the algebra is cleaner when tracked globally:
Total satisfied = Σ_c satisfied(c) = m_C + Σ_e w(e)·cut(e)
where m_C is a constant (number of Case C clauses that are automatically counted). The key property: maximizing total satisfied ↔ maximizing weighted cut value. The constant m_C only shifts the objective.
Solution extraction
From the MaxCut partition config: uᵢ = TRUE iff config[i] = config[0] (same side as s).
Size Overhead
num_verticesnum_vars + 1num_edgesnum_vars + num_clausesNote: Upper bound. Each clause contributes to at most 3 edges (Case A/B: two s-edges + one variable-edge; Case C: one variable-edge). After accumulation, at most n s-edges + min(m, n(n−1)/2) variable-variable edges survive. Safe upper bound: n + m.
Example
Source (Maximum2Satisfiability):
n = 3 variables (u₁, u₂, u₃), m = 5 clauses:
Weight accumulation:
Edge (v₁, v₃) has weight 0, so it is omitted.
Target (×2 integer weights): MaxCut with 4 vertices {s(0), v₁(1), v₂(2), v₃(3)}, 4 edges (omitting zero-weight):
Optimal assignment: u₁=T, u₂=T, u₃=T satisfies all 5 clauses:
Constant C₀ (×2 scaled): K_C values: C1=1, C2=2, C3=2, C4=1, C5=1. Total C₀ = 7 (in ×2 scale) = 3.5 (unscaled).
Partition for u₁=T, u₂=T, u₃=T: config = [0, 0, 0, 0] (all same side as s).
The affine relationship total_satisfied = C₀ + Σ w(i,j)·cut(i,j) holds for each partition. The maximizers align: the partition maximizing cut also maximizes satisfied clauses. Verified computationally on all 2⁴ = 16 partitions.
Implementation Note
The existing NAESatisfiability → MaxCut reduction uses a 2n-vertex (paired literal) construction. This reduction uses an n+1 vertex construction instead, because the OR semantics of MAX-2-SAT clauses requires breaking the literal-pair symmetry with an auxiliary vertex. Both approaches target
MaxCut<SimpleGraph, i32>.Validation Method
References