[Model] Maximum2Satisfiability

[isPANN]

Motivation

MAXIMUM 2-SATISFIABILITY (P257) from Garey & Johnson, A9 LO5. A classical NP-hard optimization problem. MAX-2-SAT serves as a key source for reductions to graph optimization problems:

• As source: R35 (→ GraphPartitioning), R37 (→ MaxCut), R157 (→ OpenHemisphere), R268 (→ MaximumBipartiteSubgraph)
• As target: R201 (3SAT →)

Definition

Name: Maximum2Satisfiability
Reference: Garey & Johnson, Computers and Intractability, A9 LO5

Mathematical definition:

INSTANCE: Set U of variables, collection C of clauses over U such that each clause c ∈ C has |c| = 2.
OBJECTIVE: Find a truth assignment for U that maximizes the number of simultaneously satisfied clauses in C.

Variables

• Count: n = |U| (one binary variable per boolean variable in U)
• Per-variable domain: {0, 1} — 0 represents FALSE, 1 represents TRUE
• Meaning: x_i = 1 if variable u_i is assigned TRUE, x_i = 0 if FALSE. The objective is to maximize the number of satisfied clauses (each clause is a disjunction of exactly 2 literals).

Schema (data type)

Type name: Maximum2Satisfiability
Variants: none

Field	Type	Description
clauses	Vec<(Literal, Literal)>	Collection of 2-literal clauses; each clause is a disjunction of exactly 2 literals
num_variables	usize	Number of boolean variables in U

Where Literal encodes a variable index and its sign (positive or negated).

Complexity

• Best known exact algorithm: Williams (2004) reduces MAX-2-SAT to MAX TRIANGLE via fast matrix multiplication, achieving O*(2^(0.7905 · n)) time, where n is the number of variables. This uses the current best matrix multiplication exponent ω < 2.3714 (Alman, Duan, Williams, Xu, Xu, Zhou, 2024), giving ω/3 ≈ 0.7905. Branch-and-bound algorithms by Shen and Zhang (2005) achieve bounds parameterized by the number of clauses m, progressing from O(m · 2^(m/3.44)) to O(m · 2^(m/5)). [Williams, "Maximum 2-satisfiability", Encyclopedia of Algorithms, 2004; Shen & Zhang, "Improving exact algorithms for MAX-2-SAT", Annals of Mathematics and AI, 2005.]

Extra Remark

Full book text:

INSTANCE: Set U of variables, collection C of clauses over U such that each clause c∈C has |c|=2, positive integer K≤|C|.
QUESTION: Is there a truth assignment for U that simultaneously satisfies at least K of the clauses in C?
Reference: [Garey, Johnson, and Stockmeyer, 1976]. Transformation from 3SAT.
Comment: Solvable in polynomial time if K=|C| (e.g.,see [Even, Itai, and Shamir, 1976]).

Note: The original G&J formulation is a decision problem with threshold K. We use the equivalent optimization formulation: maximize the number of satisfied clauses.

How to solve

• It can be solved by (existing) bruteforce. (Enumerate all 2^n truth assignments; count satisfied clauses for each; return the maximum.)
• It can be solved by reducing to integer programming. (Binary ILP: for each clause introduce a binary indicator; maximize sum of indicators subject to clause constraints.) See companion issue [Rule] Maximum2Satisfiability to ILP #961.
• Other: When all clauses must be satisfied simultaneously, reduces to 2-SAT which is solvable in polynomial time.

Reduction Rule Crossref

• [Rule] Maximum2Satisfiability to ILP #961 — [Rule] Maximum2Satisfiability to ILP (direct ILP formulation)

Example Instance

Input:
Variables: U = {x_1, x_2, x_3, x_4} (n = 4)
Clauses (7 clauses, each with exactly 2 literals):

1. (x_1 ∨ x_2)
2. (x_1 ∨ ¬x_2)
3. (¬x_1 ∨ x_3)
4. (¬x_1 ∨ ¬x_3)
5. (x_2 ∨ x_4)
6. (¬x_3 ∨ ¬x_4)
7. (x_3 ∨ x_4)

Why no assignment satisfies all 7:
Clauses {1, 2} = (x_1 ∨ x_2) and (x_1 ∨ ¬x_2) form a complementary pair on x_2: if x_1 = FALSE, then exactly one of these two clauses fails (depending on x_2). Similarly, clauses {3, 4} = (¬x_1 ∨ x_3) and (¬x_1 ∨ ¬x_3) form a complementary pair on x_3: if x_1 = TRUE, then exactly one of these two fails. Regardless of x_1's value, at least one complementary pair loses a clause, so at most 6 out of 7 can be satisfied.

Optimal assignment (6 out of 7):
x_1 = TRUE, x_2 = TRUE, x_3 = FALSE, x_4 = TRUE

1. (T ∨ T) = T ✓
2. (T ∨ F) = T ✓
3. (F ∨ F) = F ✗
4. (F ∨ T) = T ✓
5. (T ∨ T) = T ✓
6. (T ∨ F) = T ✓
7. (F ∨ T) = T ✓

Expected Outcome

Optimal value: Max(6) — the maximum number of simultaneously satisfiable clauses is 6. There are 6 optimal assignments in total (3 with x_1 = TRUE and 3 with x_1 = FALSE), confirming that x_1 is not forced.

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem, but ILP solvability claimed without companion [Rule] issue
Non-trivial	✅ Pass	Distinct optimization problem vs existing KSatisfiability (decision/feasibility)
Correctness	⚠️ Warn	References verified; complexity uses symbolic omega instead of concrete numeric value; example reasoning contains an error
Well-written	❌ Fail	Missing sections; complexity expression not concrete; example reasoning flawed

Overall: 1 passed, 2 warnings, 1 failed

---

Usefulness

Pass with warning. The problem does not exist in the codebase. Maximum2Satisfiability (MAX-2-SAT) is genuinely distinct from KSatisfiability/K2 (2-SAT): the former is an NP-hard optimization problem (maximize satisfied clauses), while the latter is a polynomial-time decision/feasibility problem. The issue lists concrete planned reductions (R35, R37, R157, R268 as source; R201 as target), which is good.

Warning: The issue claims ILP solvability ("It can be solved by reducing to integer programming") but does not link a companion [Rule] Maximum2Satisfiability to ILP issue. Per project conventions, if direct ILP solving is claimed, a companion rule issue must be linked.

Non-trivial

Pass. MAX-2-SAT has a genuinely different objective function (maximize number of satisfied clauses) compared to all existing satisfiability problems in the codebase (Satisfiability, KSatisfiability, NAESatisfiability), which are feasibility/decision problems. The optimization structure is fundamentally different.

Correctness

Pass with warnings.

References verified:

• Shen & Zhang, "Improving exact algorithms for MAX-2-SAT", Annals of Mathematics and AI, 2005 -- Confirmed. Published in volume 44, pages 419-436. The paper studies branch-and-bound improvements for MAX-2-SAT.
• Williams, "Maximum 2-satisfiability", Encyclopedia of Algorithms, 2004 -- Confirmed. Available at MIT CSAIL and Springer.
• Garey, Johnson, and Stockmeyer NP-completeness proof -- Confirmed. MAX-2-SAT is indeed NP-complete.

Warning on complexity expression: The issue states the complexity as O*(2^(omega*n/3)) with omega ≈ 2.376. Two problems:

1. The project requires concrete numeric values only in complexity strings — no symbolic constants like omega. The expression should be something like "2^(0.7905 * num_variables)" (using the current best omega < 2.3714, giving 2.3714/3 = 0.7905).
2. The Coppersmith-Winograd bound omega ≈ 2.376 is outdated. The current best (as of SODA 2025) is omega < 2.3713 (Alman, Duan, Williams, Xu, Xu, Zhou).

Warning on example reasoning: The issue claims "Clauses 1-2 force x_1 = T" — this is incorrect. Setting x_1 = FALSE also achieves the optimum of 6 satisfied clauses. For instance, (x_1=F, x_2=T, x_3=T, x_4=F) satisfies 6 clauses. The final answer (optimum = 6) is correct, but the reasoning about why is flawed.

Well-written

Fail. Several issues need correction:

1. Missing "Expected Outcome" as explicit section. The template expects a clear "Expected Outcome" section separate from the example walkthrough. The issue embeds the answer within the example but should explicitly state the optimal objective value.

2. Complexity expression uses symbolic omega. Per CLAUDE.md: "Use only concrete numeric values — no symbolic constants (epsilon, omega); inline the actual numbers with citations." The complexity section must provide a concrete expression like 2^(0.7905 * n) with citation.

3. Flawed example reasoning. The claim "Clauses 1-2 force x_1 = T" is mathematically incorrect. Both x_1 = TRUE and x_1 = FALSE can achieve the optimum of 6. The reasoning needs to be corrected or replaced with an accurate analysis.

4. ILP companion issue not linked. The "How to solve" section checks ILP but the "Reduction Rule Crossref" section (not present) does not link a companion [Rule] Maximum2Satisfiability to ILP issue.

5. GJ reference "P257" not verifiable. The page number claim could not be independently verified. The GJ designation "LO5" for MAXIMUM SATISFIABILITY is consistent with the GJ classification system (Logic section), but the specific page number should be double-checked.

Recommendations

• Replace the complexity expression with a concrete numeric value: "2^(0.7905 * num_variables)" citing Williams 2005 and the current best omega bound.
• Fix the example reasoning to accurately explain why at most 6 clauses can be satisfied (the pair {3,4} or the pair {1,2} each forces exactly one failure, so 7 is unreachable; both x_1=T and x_1=F achieve 6).
• Create and link a companion [Rule] Maximum2Satisfiability to ILP issue, or remove the ILP claim from "How to solve".
• The Shen & Zhang results are parameterized by m (number of clauses), while Williams' result is parameterized by n (number of variables). Consider citing both bounds clearly.

[isPANN]

Converted from decision framing (threshold K) to optimization framing: maximize the number of satisfied clauses. Removed K from the definition, updated the example to show optimal value Max(6), and adjusted the 'How to solve' section accordingly. The original G&J decision formulation is preserved in the Extra Remark section for reference.

[isPANN]

Issue Quality Check — Model (Re-check)

Check	Result	Details
Usefulness	⚠️ Warn	Novel problem; ILP solvability claimed without companion [Rule] issue
Non-trivial	✅ Pass	Distinct optimization problem vs existing feasibility-based SAT problems
Correctness	⚠️ Warn	References verified; complexity uses symbolic ω instead of concrete value; example reasoning flawed
Well-written	❌ Fail	Complexity not concrete; example reasoning incorrect; ILP companion not linked

Overall: 1 passed, 2 warnings, 1 failed

Previous check (2026-03-29): 1 passed, 2 warnings, 1 failed → no change.

---

Usefulness

Pass with warning. Maximum2Satisfiability does not exist in the codebase. It is genuinely distinct from existing SAT problems (Satisfiability, KSatisfiability, NAESatisfiability) which are all feasibility/decision problems. The issue lists concrete planned reductions (R35, R37, R157, R268 as source; R201 as target).

Warning: ILP solvability is claimed in "How to solve" but no companion [Rule] Maximum2Satisfiability to ILP issue is linked.

Non-trivial

Pass. MAX-2-SAT has a genuinely different objective function (maximize number of satisfied clauses) compared to all existing problems. Not a variant or renaming.

Correctness

Pass with warnings.

References verified:

• Williams, "Maximum 2-satisfiability", Encyclopedia of Algorithms, 2004 — Confirmed. Key result: O(m · 2^(ωn/3)) time via reduction to MAX TRIANGLE + fast matrix multiplication.
• Shen & Zhang, "Improving exact algorithms for MAX-2-SAT", Annals of Mathematics and AI, 2005 — Confirmed. Branch-and-bound bounds parameterized by m (number of clauses).
• Garey, Johnson, and Stockmeyer NP-completeness proof — Confirmed.

Warning — complexity uses symbolic ω: The issue states O*(2^(omega*n/3)) with omega ≈ 2.376. Two problems:

1. Project requires concrete numeric values only — no symbolic constants. Should be "2^(0.7905 * num_variables)" (using current best ω < 2.3714, giving 2.3714/3 ≈ 0.7905).
2. The cited ω ≈ 2.376 (Coppersmith-Winograd) is outdated. Current best is ω < 2.3714 (Alman, Duan, Williams, Xu, Xu, Zhou, 2024).

Warning — example reasoning error: The claim "Clauses 1-2 force x₁ = T" is incorrect. Python verification shows that x₁ = FALSE also achieves the optimum of 6 satisfied clauses. There are 6 optimal assignments total, 3 with x₁=T and 3 with x₁=F. The optimal value (Max(6)) is correct, but the reasoning is wrong.

Well-written

Fail. Issues to fix:

1. Complexity uses symbolic omega. Must use concrete numeric value: "2^(0.7905 * num_variables)" citing Williams 2004 with current ω < 2.3714.

2. Example reasoning is incorrect. "Clauses 1-2 force x₁ = T" is wrong — both x₁=T and x₁=F achieve the optimum. The correct reasoning: clauses 3-4 form the pair (¬x₁ ∨ x₃) and (¬x₁ ∨ ¬x₃), and clauses 1-2 form the pair (x₁ ∨ x₂) and (x₁ ∨ ¬x₂). Each pair forces exactly one failure when its "controlling" variable takes the value that makes both first-literals false. Since these pairs share no variables beyond x₁, any assignment fails at least one clause from one of these pairs, so at most 6 out of 7 can be satisfied.

3. ILP companion issue not linked. Either create and link a [Rule] Maximum2Satisfiability to ILP issue, or remove the ILP claim from "How to solve".

4. Missing explicit Expected Outcome section. The optimal value is embedded in the example but should be in a separate section per template.

Recommendations

• Use complexity string "2^(0.7905 * num_variables)" with citation: Williams 2004, using ω < 2.3714 (Alman et al., 2024).
• Fix example reasoning to correctly explain why at most 6 clauses can be satisfied.
• The Shen & Zhang bound O(m · 2^(m/5)) is parameterized by clauses m, while Williams' is by variables n — consider citing both clearly and picking the variable-based bound for the complexity string.

[isPANN]

Fix-issue changelog

• Complexity: replaced symbolic omega ≈ 2.376 with concrete 2^(0.7905 * n) using current best ω < 2.3714 (Alman et al., 2024)
• Example reasoning: rewrote incorrect "Clauses 1-2 force x₁ = T" to correct complementary-pair explanation (both x₁=T and x₁=F achieve optimum)
• Expected Outcome: added explicit section with Max(6) and note about 6 optimal assignments
• ILP companion: created [Rule] Maximum2Satisfiability to ILP #961 [Rule] Maximum2Satisfiability to ILP and linked in "Reduction Rule Crossref" section
• How to solve: updated ILP bullet to reference companion issue [Rule] Maximum2Satisfiability to ILP #961

Applied by /fix-issue.