[Rule] Satisfiability → Maximum2Satisfiability

[isPANN]

Source: Satisfiability
Target: Maximum2Satisfiability
Motivation: Establishes NP-hardness of Maximum 2-Satisfiability by reduction from general SAT. This is the standard Garey-Johnson-Stockmeyer (1976) gadget construction that converts each k-literal clause into O(k) 2-literal clauses with auxiliary variables, preserving satisfiability as a threshold on the number of satisfied 2-clauses. This gives Maximum2Satisfiability its first incoming reduction.
Reference: Garey & Johnson, Computers and Intractability, LO5, p.259; Garey, Johnson, and Stockmeyer (1976).

GJ Source Entry

[LO5] MAXIMUM 2-SATISFIABILITY
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|.

Note: While GJ references 3SAT as the source, we reduce from general Satisfiability (arbitrary clause lengths). Each clause of length k is expanded to 10 2-clauses using the standard k=3 gadget after first padding to length 3.

Reduction Algorithm

Given a Satisfiability instance with n variables and m clauses of arbitrary length, construct a Maximum2Satisfiability instance.

Step 1 — Normalize to 3-literal clauses

For each source clause C of length k:

• k = 1 (unit clause (l₁)): Introduce 2 fresh variables y, z and create clause (l₁ ∨ y ∨ z), (l₁ ∨ y ∨ ¬z), (l₁ ∨ ¬y ∨ z), (l₁ ∨ ¬y ∨ ¬z). The conjunction is satisfiable iff l₁ = TRUE (each 3-clause is treated independently in Step 2).

• k = 2 (clause (l₁ ∨ l₂)): Introduce 1 fresh variable y and create (l₁ ∨ l₂ ∨ y) and (l₁ ∨ l₂ ∨ ¬y).

• k = 3: Already in the right form.

• k > 3: Apply the standard linear expansion: introduce k−3 fresh variables y₁, ..., y_{k−3} and create:

  • (l₁ ∨ l₂ ∨ y₁)
  • (¬y₁ ∨ l₃ ∨ y₂)
  • (¬y₂ ∨ l₄ ∨ y₃)
  • ...
  • (¬y_{k−3} ∨ l_{k−1} ∨ lₖ)

  This produces k−2 clauses of length 3. The conjunction is satisfiable iff the original clause is satisfied.

After Step 1, we have m' 3-literal clauses and n' = n + (auxiliary variables introduced) total variables.

Step 2 — Convert each 3-literal clause to 10 MAX-2-SAT clauses (GJS gadget)

For each 3-literal clause (l₁ ∨ l₂ ∨ l₃), introduce one fresh auxiliary variable wⱼ and create 10 clauses:

#	Clause	Role
1	(l₁)	unit: reward literal 1
2	(l₂)	unit: reward literal 2
3	(l₃)	unit: reward literal 3
4	(wⱼ)	unit: reward auxiliary
5	(¬l₁ ∨ ¬l₂)	penalize both-true pair
6	(¬l₂ ∨ ¬l₃)	penalize both-true pair
7	(¬l₁ ∨ ¬l₃)	penalize both-true pair
8	(l₁ ∨ ¬wⱼ)	link auxiliary to literal 1
9	(l₂ ∨ ¬wⱼ)	link auxiliary to literal 2
10	(l₃ ∨ ¬wⱼ)	link auxiliary to literal 3

Key property (exhaustive case analysis):

• If the original 3-clause IS satisfied (≥ 1 literal true): with optimal wⱼ choice, exactly 7 of the 10 clauses are satisfied.
• If the original 3-clause is NOT satisfied (all 3 literals false): at most 6 of the 10 clauses can be satisfied.

Therefore: the source SAT formula is satisfiable ↔ the MAX-2-SAT optimum equals 7 · m' (all normalized clauses satisfied).

Case table for one GJS gadget:

l₁	l₂	l₃	Clause sat?	Best wⱼ	Satisfied
F	F	F	No	F	6/10
F	F	T	Yes	F	7/10
F	T	F	Yes	F	7/10
F	T	T	Yes	T	7/10
T	F	F	Yes	F	7/10
T	F	T	Yes	T	7/10
T	T	F	Yes	T	7/10
T	T	T	Yes	T	7/10

Solution extraction

Restrict the MAX-2-SAT optimal assignment to the original n variables. Discard all auxiliary variables (from both Step 1 and Step 2).

Correctness

(Forward) A satisfying assignment for the source SAT instance satisfies all normalized 3-clauses, so each GJS gadget achieves 7/10, yielding total = 7m'. With the right wⱼ choices, the MAX-2-SAT optimum is exactly 7m'.

(Backward) If the MAX-2-SAT optimum is 7m', every GJS gadget achieves 7/10, meaning every 3-clause is satisfied. By the soundness of the normalization (Step 1), every original source clause is satisfied. Restricting to original variables yields a satisfying assignment.

If the source is unsatisfiable, at least one 3-clause is unsatisfied, so at least one gadget achieves ≤ 6/10, giving total < 7m'.

Size Overhead

Target metric (code name)	Expression
num_vars	num_vars + num_clauses + num_literals
num_clauses	10 * num_clauses + 10 * num_literals

Derivation: Step 1 normalization of a clause of length k produces at most k−2 auxiliary variables and k−2 three-literal clauses. Total auxiliary from Step 1 ≤ Σ(kᵢ − 2) ≤ num_literals. Total 3-clauses ≤ Σ max(kᵢ − 2, 2) ≤ num_literals + num_clauses (accounting for k=1,2 padding). Step 2 adds one auxiliary per 3-clause. Total MAX-2-SAT variables ≤ n + num_literals + (num_literals + num_clauses). Total MAX-2-SAT clauses = 10 · (number of 3-clauses) ≤ 10 · (num_literals + num_clauses).

Example

Source (Satisfiability):
n = 3 variables (x₁, x₂, x₃), m = 2 clauses:

• C₁ = (x₁ ∨ ¬x₂ ∨ x₃) — length 3
• C₂ = (¬x₁ ∨ x₂) — length 2

Step 1 — Normalize:

• C₁ already has 3 literals: (x₁ ∨ ¬x₂ ∨ x₃)
• C₂ has 2 literals: introduce fresh y₁, create (¬x₁ ∨ x₂ ∨ y₁) and (¬x₁ ∨ x₂ ∨ ¬y₁)

After normalization: n' = 4 variables (x₁, x₂, x₃, y₁), m' = 3 three-literal clauses.

Step 2 — GJS gadgets: Introduce w₁, w₂, w₃ (one per 3-clause). Total variables: 4 + 3 = 7.

For C₁ = (x₁ ∨ ¬x₂ ∨ x₃), auxiliary w₁:

1. (x₁), 2. (¬x₂), 3. (x₃), 4. (w₁), 5. (¬x₁ ∨ x₂), 6. (x₂ ∨ ¬x₃), 7. (¬x₁ ∨ ¬x₃), 8. (x₁ ∨ ¬w₁), 9. (¬x₂ ∨ ¬w₁), 10. (x₃ ∨ ¬w₁)

For (¬x₁ ∨ x₂ ∨ y₁), auxiliary w₂:

1. (¬x₁), 2. (x₂), 3. (y₁), 4. (w₂), 5. (x₁ ∨ ¬x₂), 6. (¬x₂ ∨ ¬y₁), 7. (x₁ ∨ ¬y₁), 8. (¬x₁ ∨ ¬w₂), 9. (x₂ ∨ ¬w₂), 10. (y₁ ∨ ¬w₂)

For (¬x₁ ∨ x₂ ∨ ¬y₁), auxiliary w₃:

1. (¬x₁), 2. (x₂), 3. (¬y₁), 4. (w₃), 5. (x₁ ∨ ¬x₂), 6. (¬x₂ ∨ y₁), 7. (x₁ ∨ y₁), 8. (¬x₁ ∨ ¬w₃), 9. (x₂ ∨ ¬w₃), 10. (¬y₁ ∨ ¬w₃)

Target: Maximum2Satisfiability with 7 variables, 30 clauses.

Satisfying assignment: x₁=T, x₂=T, x₃=T satisfies both original clauses.

• C₁: (T ∨ F ∨ T) = T
• C₂: (F ∨ T) = T

After normalization, all three 3-clauses are satisfied. Each gadget achieves 7/10. Total = 21 = 7 · 3 = 7m'. ✓

Optimal auxiliary choices: For C₁ gadget with x₁=T, x₂=T (¬x₂=F), x₃=T (all true): best w₁=T → 7/10.

Extracted source solution: x₁=T, x₂=T, x₃=T → both original clauses satisfied. ✓

Validation Method

• Closed-loop test: reduce SAT to MAX-2-SAT, solve MAX-2-SAT with brute force, extract solution on original variables, verify all source clauses satisfied
• Verify optimality: optimal MAX-2-SAT value = 7m' ↔ source is satisfiable; < 7m' ↔ unsatisfiable
• Test with: length-1 clauses, length-2 clauses, length-3 clauses, length-4+ clauses, mixed lengths
• Test with both satisfiable and unsatisfiable SAT instances

References

• Garey, M. R., Johnson, D. S., and Stockmeyer, L. (1976). "Some simplified NP-complete graph problems." Theoretical Computer Science 1, pp. 237–267.
• Garey, M. R. & Johnson, D. S. (1979). Computers and Intractability, LO5, p. 259.

[isPANN]

Issue Quality Check — Model

Check	Result	Details
Usefulness	❌ Fail	Issue body does not define MinimumDisjunctiveNormalForm; contains unrelated rule content
Non-trivial	❌ Fail	Cannot evaluate — no model definition present
Correctness	❌ Fail	Cannot evaluate — no model definition present
Well-written	❌ Fail	Title/body mismatch; all required Model sections missing

Overall: 0 passed, 0 warnings, 4 failed

---

Usefulness

The issue title is [Model] MinimumDisjunctiveNormalForm, but the issue body contains an entirely different issue: a [Rule] reduction from 3SAT to Maximum 2-Satisfiability (MAX-2-SAT). There is no definition, schema, variables, complexity, or example for MinimumDisjunctiveNormalForm anywhere in the body. The problem does not exist in the codebase (pred show MinimumDisjunctiveNormalForm fails), so the model itself could potentially be useful — but this issue does not actually propose it.

Non-trivial

Cannot evaluate. The issue body contains no model definition for MinimumDisjunctiveNormalForm; it describes a reduction between two other problems (3SAT and MAX-2-SAT).

Correctness

Cannot evaluate. The references (Garey, Johnson, and Stockmeyer 1976; Even, Itai, and Shamir 1976) and the reduction algorithm in the body are about MAX-2-SAT, not MinimumDisjunctiveNormalForm. The cited reference garey1976 does exist in the project bibliography and is a legitimate paper ("Some simplified NP-complete graph problems", Theoretical Computer Science 1, pp. 237-267), but it is being cited for an issue that does not match the title.

The reduction described (3SAT to MAX-2-SAT with 10 clauses per gadget, threshold 7m) appears to be a correct and well-known construction from the literature. However, it belongs in a [Rule] issue, not a [Model] issue for MinimumDisjunctiveNormalForm.

Well-written

Critical structural failure: The title and body are completely mismatched. The title says [Model] MinimumDisjunctiveNormalForm but the body is a [Rule] issue template describing a 3SAT to Maximum 2-Satisfiability reduction.

All required Model template sections are missing:

Section	Status
Motivation	Missing (body has rule motivation for MAX-2-SAT)
Name	Missing (title says MinimumDisjunctiveNormalForm but body never defines it)
Definition	Missing
Variables	Missing
Schema	Missing
Complexity	Missing
How to solve	Missing
Example Instance	Missing (body has a rule example for 3SAT to MAX-2-SAT)
Expected Outcome	Missing
Reference	Missing (references are for the wrong problem)

Recommendations

• This issue needs to be completely rewritten with the correct [Model] template for MinimumDisjunctiveNormalForm (Minimum DNF / LO6 in Garey & Johnson, Appendix A).
• The MAX-2-SAT reduction content currently in the body could be repurposed into a separate [Rule] issue if Maximum2Satisfiability is added as a model first.
• MinimumDisjunctiveNormalForm (GJ reference LO6) asks: given a Boolean function (e.g., via truth table), find a DNF expression with at most K product terms. The issue body should define this problem precisely with input, feasibility constraints, objective, variables, and a worked example.