[Rule] MaxCut/One to Maximum2Satisfiability

[isPANN]

Source

MaxCut/SimpleGraph/One

Target

Maximum2Satisfiability

Motivation

This classic affine objective encoding provides the reverse direction of the existing Maximum 2-SAT to MaxCut connection. The unit-weight source restriction is explicit and necessary because the target model is unweighted.

Reference

Gramm, Hirsch, Niedermeier, and Rossmanith, “Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT,” Discrete Applied Mathematics 130(2), 2003, DOI 10.1016/S0166-218X(02)00402-X.

Reduction Algorithm

Given unweighted G=(V,E), V={0,...,n-1}, m=|E|:

1. Create Boolean variable x_v for every vertex; its truth value is the side of the cut.
2. For every edge {u,v}, add clauses (x_u OR x_v) and (not x_u OR not x_v). In the repository's signed, 1-indexed CNFClause representation these are [u+1, v+1] and [-(u+1), -(v+1)].
3. Extract the source cut configuration directly from the target assignment: configuration position v is 1 exactly when x_v is true, and 0 otherwise.

Each edge occurrence creates its own clause pair. Consequently, parallel edges remain repeated clause pairs. A self-loop {u,u} becomes (x_u OR x_u) and (not x_u OR not x_u).

If the endpoints differ, both clauses are satisfied. If they agree, exactly one is satisfied. This also handles a self-loop, whose endpoints always agree. Therefore for every configuration

satisfied_clauses = m + cut_edges.

The affine offset is constant, so the maximizers coincide and max2sat_optimum = m + maxcut_optimum.

Size Overhead

Target metric	Formula
num_vars	num_vertices
num_clauses	2 * num_edges

Validation Method

• Exhaust every simple graph through five vertices and every cut/truth assignment.
• Check the affine objective identity for every configuration, not only at the optimum.
• Verify direct solution extraction and empty/edgeless/disconnected graphs.
• Explicitly test self-loops and parallel edges admitted by the current SimpleGraph constructor; confirm repeated literals and repeated clause pairs remain valid target data.

Example

1. Source instance: four-cycle 01,12,23,30 plus diagonal 02, giving five edges.
2. Construction: create four variables and the ten clauses (x_0 OR x_1), (not x_0 OR not x_1), (x_1 OR x_2), (not x_1 OR not x_2), (x_2 OR x_3), (not x_2 OR not x_3), (x_3 OR x_0), (not x_3 OR not x_0), (x_0 OR x_2), and (not x_0 OR not x_2).
3. Target witness: cut assignment [0,1,0,1]. The four cycle edges cross and diagonal 02 does not.
4. Round trip: source cut value is 4. The eight clauses belonging to crossing edges are all satisfied, while the diagonal contributes exactly one, so the target value is 5+4=9. Exhaustive enumeration confirms these are the respective optima; putting all vertices on one side gives target value 5 and checks the affine offset.
5. Negative-threshold check: for a graph consisting of one edge, no cut has value at least 2. Its two-clause target has optimum 2, so the corresponding target threshold m+2=3 is also unattainable.

BibTeX

@article{Gramm2003Max2SatMaxCut,
  author = {Gramm, Jens and Hirsch, Edward A. and Niedermeier, Rolf and Rossmanith, Peter},
  title = {Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT},
  journal = {Discrete Applied Mathematics},
  volume = {130},
  number = {2},
  pages = {139--155},
  year = {2003},
  doi = {10.1016/S0166-218X(02)00402-X}
}

[isPANN]

Issue Quality Check — Rule

Check	Result	Details
Usefulness	✅ Pass	Both endpoint variants exist, and the current graph has no MaxCut/SimpleGraph/One → Maximum2Satisfiability path.
Non-trivial	✅ Pass	Each graph edge is structurally encoded by two Boolean clauses, with an affine objective transformation.
Correctness	✅ Pass	The cited paper exists and Section 5 gives this exact construction and the identity MAX-2-SAT value = M + cut value; an independent paper states the same result as Theorem 5.1.
Completeness	⚠️ Warn	The construction works on all traced source instances, including loops and parallel edges admitted by the current SimpleGraph constructor, but the issue only calls out empty/edgeless/disconnected cases. Document loops and parallel edges explicitly.
Well-written	✅ Pass	All required sections are substantive; metric names match the target, extraction is clear, and the four-vertex example is non-degenerate and round-trip testable.

Overall: 4 passed, 0 failed, 1 warning

---

Usefulness

• pred show MaxCut/SimpleGraph/One --json and pred show Maximum2Satisfiability --json resolve the exact source and target. Their size fields are respectively num_vertices, num_edges and num_vars, num_clauses.
• pred path MaxCut/SimpleGraph/One Maximum2Satisfiability --json reports no reduction path, so this is a novel connection rather than a dominated direct edge.
• The Motivation identifies the reverse connection and explains why the One restriction is necessary for the unweighted target.

Non-trivial

This is a genuine structural transformation: every edge {u,v} becomes two constraints, (x_u ∨ x_v) and (¬x_u ∨ ¬x_v). The target objective is not a relabeling of the source objective; it differs by the instance-dependent constant m.

Correctness

• The bibliographic metadata matches the published article: Jens Gramm, Edward A. Hirsch, Rolf Niedermeier, and Peter Rossmanith, Discrete Applied Mathematics 130(2), 139–155 (2003), DOI 10.1016/S0166-218X(02)00402-X.
• I read the full open ECCC preprint, TR00-037, Section 5 (“Application to MAX-CUT”). It translates each edge of weight w into the two same-weight clauses (x_i ∨ x_j) and (¬x_i ∨ ¬x_j), then states that a graph of total edge weight M has a cut of weight k iff the formula has satisfiable clause weight M+k; every optimal assignment directly yields a maximum cut. Corollary 2 applies the construction to a graph with n vertices and edges of total weight M. This explicitly covers the full unit-weight source as a special case, with no additional connectivity or degree precondition. Source: ECCC TR00-037, Section 5, p. 10 and Corollary 2, p. 12.
• Independent cross-check: Haiou Shen and Hantao Zhang, “Improving Exact Algorithms for MAX-2-SAT,” Theorem 5.1, states the same two-clause construction for an undirected simple unit-weight graph and the same m+k equivalence. Published DOI: 10.1007/s10472-005-7036-z.
• Direct per-edge truth table: if x_u ≠ x_v, both clauses are true; if x_u = x_v, exactly one is true. Summing gives sat(x)=m+cut(x) for every assignment, and direct witness extraction is therefore correct.
• The small validator exhaustively checked every simple graph through five vertices and confirmed both the canonical values (MaxCut=4, MAX-2-SAT=9) and opt_target = m + opt_source throughout.

No better construction is needed for this target: n variables and 2m clauses are exactly the classic encoding used by the cited literature.

Completeness

Literature scope. Gramm et al. introduce the reduction for an undirected graph with integer edge weights and prove the weighted identity before deriving Corollary 2; the issue's unit-weight source is strictly within that scope. Shen–Zhang Theorem 5.1 independently states it for undirected simple unit-weight graphs. Neither source imposes connectedness, minimum degree, or a nonempty graph.

Codebase scope. MaxCut<SimpleGraph, One> has unrestricted binary vertex configurations. SimpleGraph::new accepts zero vertices, isolated vertices, self-loops, and parallel edges (although its type name suggests the conventional simple-graph domain). Maximum2Satisfiability::new accepts repeated clauses and repeated literals as long as each clause has length two.

Hand traces beyond the worked example:

1. Empty graph (n=0,m=0). The construction creates zero variables and zero clauses. The empty assignment has target value 0=0+0, and extraction returns the empty cut configuration.
2. One isolated vertex (n=1,m=0). It creates one variable and no clauses. Either assignment has target value zero and extracts to a source cut of value zero.
3. Self-loop {u,u} (allowed by the current constructor). It creates (x_u∨x_u) and (¬x_u∨¬x_u). Exactly one is satisfied for either truth value; the loop never crosses the cut, so 1 = m + 0 and extraction remains valid.
4. Parallel edges (also allowed by the current constructor). Each occurrence creates another identical clause pair. The target stores clauses in a Vec, so multiplicity is preserved; every occurrence contributes 1 + [x_u≠x_v], exactly matching the source's multiplicity.

The construction therefore remains correct, but the issue's Validation Method names only empty/edgeless/disconnected graphs. Please explicitly state and test self-loops and parallel edges, or make the source representation reject them. This is a warning rather than a failure because the stated construction already handles both.

For comparison, existing rules sourced from MaxCut also iterate the graph's edge list directly; notably, maxcut_minimummatrixcover.rs overwrites parallel-edge matrix entries and therefore does not provide stronger multiedge coverage to emulate.

Well-written

• All required template sections are present and implementable.
• The target metric names are correct: num_vars and num_clauses.
• n, m, the graph, variables, clauses, affine offset, and extraction are consistently defined.
• The example has five edges, crossing and non-crossing edges, multiple feasible assignments of different values, explicit source/target optima, and a direct round trip.

Recommendations

• State the implementation indexing explicitly: repository CNFClause literals are signed and 1-indexed, so vertex v∈{0,…,n−1} must use literal v+1; cut configuration positions remain 0-indexed for direct extraction.
• Add loop and parallel-edge cases to the validation list, since the current SimpleGraph constructor admits them.
• For maximum reproducibility, enumerate the ten concrete clauses in the worked example rather than only saying “two per edge.”

[isPANN]

Rule Fix

Diagnosis:

• Target-instance validity/completeness: the construction was mathematically correct, but it did not state the repository's signed, 1-indexed CNFClause encoding.
• Source-domain completeness: the body did not explicitly cover self-loops and parallel edges admitted by the current SimpleGraph constructor.
• Example coverage: the optimization example established the optimum but omitted an explicit negative-threshold instance.

Literature:

• Gramm, Hirsch, Niedermeier, and Rossmanith, ECCC TR00-037, Section 5, gives the same construction: one variable per vertex and the two clauses (x_i OR x_j) and (not x_i OR not x_j) for every edge. It proves the affine identity MAX-2-SAT value = M + cut value and direct extraction of a maximum cut. The issue's core construction does not diverge from the canonical reduction.

Changes:

• Specified the exact 1-indexed signed literal encoding and direct configuration extraction.
• Documented how self-loops and parallel edges are preserved and why the objective identity still holds.
• Enumerated the worked example's ten clauses and added a negative-threshold check.
• Expanded the validation plan to cover repeated literals and repeated clauses.

Smoke test:

• 151 checks passed across all mandatory buckets: worked example, negative threshold, boundary cases, objective agreement, extraction, overhead, and target validity.
• The checks included empty and isolated graphs, self-loops, parallel edges, 60 deterministic small instances, and exhaustive assignments per instance.

[isPANN]

Issue Quality Check — Rule — Re-check

Previously: 4 passes and 1 completeness warning. After the rule-fix edit: 5 passes and 0 warnings.

Check	Result	Details
Usefulness	✅ Pass	Both endpoint variants exist, and the current reduction graph has no MaxCut/SimpleGraph/One → Maximum2Satisfiability path.
Non-trivial	✅ Pass	Every source edge is structurally encoded by two target clauses, with an affine objective transformation.
Correctness	✅ Pass	The cited paper exists; its Section 5 gives this exact construction, objective identity, and direct witness extraction.
Completeness	✅ Pass	The edited body now explicitly covers empty, disconnected, looped, and parallel-edge instances admitted by the source representation.
Well-written	✅ Pass	All required sections are substantive, repository literal indexing is explicit, target metric names match, and the worked example is fully reproducible.

Overall: 5 passed, 0 failed, 0 warnings

---

Usefulness

• pred show resolves MaxCut/SimpleGraph/One and Maximum2Satisfiability with source metrics num_vertices, num_edges and target metrics num_vars, num_clauses.
• pred path MaxCut/SimpleGraph/One Maximum2Satisfiability --json reports no path, so this adds a novel graph edge rather than a dominated direct rule.
• The motivation explains both the reverse connection and the unit-weight restriction.

Non-trivial

Each edge occurrence becomes two Boolean constraints. The target objective differs from the source by the instance-dependent constant m, so this is a genuine structural transformation rather than relabeling or subtype coercion.

Correctness

• The article metadata matches Gramm, Hirsch, Niedermeier, and Rossmanith, Discrete Applied Mathematics 130(2), 139–155 (2003), DOI 10.1016/S0166-218X(02)00402-X.
• The open original preprint, ECCC TR00-037, Section 5, constructs one variable per vertex and the positive/negative clause pair per edge. It proves target value M+k for a cut of weight k and direct extraction of an optimal cut.
• An independent primary-source cross-check, Shen and Zhang, “Improving Exact Algorithms for MAX-2-SAT,” Theorem 5.1, states the same unit-weight construction and m+k equivalence (DOI 10.1007/s10472-005-7036-z).
• A 151-check smoke test verified the stronger pointwise identity sat(x)=m+cut(x), not only equality at the optimum.

Completeness

• The literature construction is stated for undirected integer-weighted graphs and imposes no connectedness, minimum-degree, or nonempty-input precondition; the unit-weight source is within that scope.
• Repository tracing confirms SimpleGraph::new accepts empty graphs, isolated vertices, self-loops, and parallel edges. Maximum2Satisfiability accepts repeated clauses and repeated literals when each clause has length two.
• The edited body now states the exact behavior: a loop creates complementary repeated-literal clauses and contributes the affine baseline one; every parallel-edge occurrence creates another clause pair, preserving multiplicity.
• Smoke coverage included empty and isolated graphs, loops, parallel edges, and 60 deterministic small instances with exhaustive assignments.

Well-written

• The implementation mapping is unambiguous: source vertex v uses signed target literal ±(v+1), while extracted configuration positions remain 0-indexed.
• The overhead formulas use the target's exact metric names and match construction counts.
• The four-vertex example enumerates all ten clauses, contains both crossing and non-crossing edges, demonstrates source and target optima, and includes a negative-threshold sanity check.

Recommendations

• None required before implementation.