[Rule] KSatisfiability to MaxCut

[zazabap]

Source: KSatisfiability
Target: MaxCut
Motivation: Classic NP-completeness reduction connecting Boolean satisfiability to graph partitioning, establishing MaxCut as NP-hard.
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 3-SAT instance with $n$ variables $x_1, \ldots, x_n$ and $m$ clauses $C_1, \ldots, C_m$:

Notation:

• $n$ = number of variables, $m$ = number of clauses (each clause has exactly 3 literals)
• For variable $x_i$, create two vertices: $v_i$ (positive literal) and $v_i'$ (negative literal)

Variable mapping (variable gadgets):

1. For each variable $x_i$, create two vertices $v_i$ and $v_i'$ representing $x_i$ and $\neg x_i$.
2. Connect $v_i$ and $v_i'$ with an edge of weight $m$. This forces them onto opposite sides of any large cut, encoding that a variable and its negation have opposite truth values.

This gives $2n$ vertices and $n$ edges from variable gadgets.

Constraint/objective transformation (clause gadgets):
3. For each clause $C_j = (\ell_a \lor \ell_b \lor \ell_c)$:

• Add a triangle (3 edges, weight 1 each) connecting the three literal-vertices.
• For each literal $\ell$ in the clause, add an edge of weight 1 between the literal-vertex and its complement-vertex (these accumulate onto the variable-gadget edges when parallel edges are merged).

4. Cut threshold: The instance is satisfiable iff the maximum cut value $\geq n \cdot m + 2m$. Each variable gadget contributes $m$ + (number of occurrences) from the forced-opposite edges; each satisfied clause contributes exactly 2 from its triangle.

Solution extraction: For variable $x_i$, if $v_i$ is on side $S$ of the partition, set $x_i = \text{true}$; otherwise $\text{false}$. The complement vertex $v_i'$ will be on the opposite side in any optimal cut.

Size Overhead

Target metric (code name)	Polynomial (using symbols above)
num_vertices	$2n$
num_edges	$n + 6m$ (variable-gadget base edges + 3 triangle edges + 3 complement edges per clause; parallel edges merged by summing weights)

Validation Method

• Construct small 3-SAT instances, reduce to MaxCut, solve both with BruteForce.
• Verify that satisfying assignments map to maximum cuts, and unsatisfiable instances have strictly smaller maximum cut.
• Test with both satisfiable and unsatisfiable instances.

Example

Source: 3-SAT with $n=3$, $m=2$

• Variables: $x_1, x_2, x_3$
• $C_1 = (x_1 \lor x_2 \lor x_3)$
• $C_2 = (\neg x_1 \lor \neg x_2 \lor x_3)$

Reduction:

• Vertices: $v_1, v_1', v_2, v_2', v_3, v_3'$ (6 vertices total)
• Variable gadget edges: $(v_1, v_1')$ $w=2$, $(v_2, v_2')$ $w=2$, $(v_3, v_3')$ $w=2$
• $C_1$ triangle: $(v_1, v_2)$ $w=1$, $(v_2, v_3)$ $w=1$, $(v_1, v_3)$ $w=1$
• $C_1$ complement edges: add $w \mathrel{+}= 1$ to $(v_1, v_1')$, $(v_2, v_2')$, $(v_3, v_3')$
• $C_2$ triangle: $(v_1', v_2')$ $w=1$, $(v_2', v_3)$ $w=1$, $(v_1', v_3)$ $w=1$
• $C_2$ complement edges: add $w \mathrel{+}= 1$ to $(v_1', v_1)$, $(v_2', v_2)$, $(v_3, v_3')$
• Final variable gadget weights: $(v_1, v_1')$ $w=4$, $(v_2, v_2')$ $w=4$, $(v_3, v_3')$ $w=4$

Solution: $x_1=\text{T}$, $x_2=\text{F}$, $x_3=\text{T}$ satisfies both clauses. Partition $S={v_1, v_2', v_3}$, complement $={v_1', v_2, v_3'}$. The cut crosses all variable-gadget edges (contributing 12) plus clause triangle edges that span the partition.