[Rule] Maximum2Satisfiability to ILP #961
Description
Motivation
Direct ILP formulation for Maximum 2-Satisfiability. Companion issue for #807 (Maximum2Satisfiability model). Enables ILP-based solving for MAX-2-SAT instances.
Source
Maximum2Satisfiability
Target
ILP (Integer Linear Programming)
Reference
Standard binary ILP formulation for MAX-SAT; see Wolsey, Integer Programming, Chapter 1.
Reduction Algorithm
Input: A MAX-2-SAT instance with variables U = {u₁, ..., uₙ} and clauses C = {c₁, ..., cₘ}, where each clause cⱼ is a disjunction of exactly 2 literals.
- Create binary decision variables x₁, ..., xₙ ∈ {0, 1} corresponding to the truth assignment (xᵢ = 1 means uᵢ = TRUE).
- For each clause cⱼ, create a binary indicator variable zⱼ ∈ {0, 1} (zⱼ = 1 means clause cⱼ is satisfied).
- For each clause cⱼ = (ℓₐ ∨ ℓᵦ), add the constraint:
- zⱼ ≤ ℓ̃ₐ + ℓ̃ᵦ, where ℓ̃ᵢ = xᵢ if the literal is positive, or (1 - xᵢ) if negated.
- Objective: maximize ∑ⱼ zⱼ.
Solution extraction: Read the optimal x₁, ..., xₙ values as the truth assignment.
Size Overhead
| Code metric | Formula |
|---|---|
num_variables |
n + m |
num_constraints |
m |
Where n = number of boolean variables, m = number of clauses.
Validation Method
Closed-loop test: construct a MAX-2-SAT instance, reduce to ILP, solve the ILP, extract the truth assignment, verify it maximizes satisfied clauses.
Example
Source: MAX-2-SAT with U = {x₁, x₂, x₃}, clauses: (x₁ ∨ x₂), (¬x₁ ∨ x₃), (¬x₂ ∨ ¬x₃), (x₁ ∨ ¬x₃)
ILP formulation:
- Variables: x₁, x₂, x₃ ∈ {0,1}, z₁, z₂, z₃, z₄ ∈ {0,1}
- Constraints:
- z₁ ≤ x₁ + x₂
- z₂ ≤ (1-x₁) + x₃
- z₃ ≤ (1-x₂) + (1-x₃)
- z₄ ≤ x₁ + (1-x₃)
- Objective: maximize z₁ + z₂ + z₃ + z₄
Optimal: x₁=1, x₂=1, x₃=0 → all 4 clauses satisfied → Max(4).