MAX 2-SAT is NP-complete

MaxTwoSAT consists of instances x : MaxTwoSATInstance (Cslib.Complexity.encMaxTwoSAT) pairing a formula x.formula in conjunctive normal form with at most two literals per clause and a target x.target such that some assignment satisfies at least x.target clauses of x.formula, counted with multiplicity. Garey, Johnson and Stockmeyer proved it NP-complete Garey, Johnson and Stockmeyer (attribution from secondary sources; the theorem number is not checked against the paper), although 2-satisfiability itself is in NL (Cslib.Complexity.TwoSAT.mem_NL).

The reduction is their ten-clause gadget. For a clause a ∨ b ∨ c and a fresh variable w, the formula MaxTwoSAT.gadget a b c w has the ten clauses a, b, c, w, ¬a ∨ ¬b, ¬a ∨ ¬c, ¬b ∨ ¬c, a ∨ ¬w, b ∨ ¬w, c ∨ ¬w. Every assignment satisfies at most seven of them; some value of w reaches seven exactly when the assignment satisfies a ∨ b ∨ c, and otherwise at most six are satisfied (MaxTwoSAT.gadgetScore). The table depends only on the truth values of a, b, c, so repeated literals are harmless. The reduction toMaxTwoSAT starts from ExactThreeSAT, doubles the source variables so that the odd numbers are fresh, puts one gadget on each clause, and asks for seven satisfied clauses per gadget; a formula with a clause of another width becomes a fixed no-instance. Composed with the padding toExactThreeSAT, which repeats a literal of every clause of one or two literals, this reduces ThreeSAT to MaxTwoSAT.

Main definitions

• Cslib.Complexity.MaxTwoSATInstance, Cslib.Complexity.encMaxTwoSAT.
• Cslib.Complexity.MaxTwoSAT: the decision version of maximum 2-satisfiability.
• Cslib.Complexity.MaxTwoSAT.gadget: the ten-clause gadget of one clause.
• Cslib.Complexity.toMaxTwoSAT: the reduction from ExactThreeSAT.

Main results

• Cslib.Complexity.MaxTwoSAT.mem_NP: MaxTwoSAT ∈ NP encMaxTwoSAT.
• Cslib.Complexity.MaxTwoSAT.countP_gadget: the satisfied clauses of one gadget, counted by MaxTwoSAT.gadgetScore.
• Cslib.Complexity.MaxTwoSAT.gadgetScore_le, Cslib.Complexity.MaxTwoSAT.gadgetScore_majority, Cslib.Complexity.MaxTwoSAT.gadgetScore_false_le: at most seven, seven when the clause holds and the fresh variable is the majority, at most six when the clause fails.
• Cslib.Complexity.mem_MaxTwoSAT_toMaxTwoSAT_iff: correctness of the reduction.
• Cslib.Complexity.polyTimeReducible_ExactThreeSAT_MaxTwoSAT, Cslib.Complexity.polyTimeReducible_ThreeSAT_MaxTwoSAT: ExactThreeSAT and ThreeSAT reduce to MaxTwoSAT.
• Cslib.Complexity.MaxTwoSAT_npComplete: MaxTwoSAT is NP-complete.

References

• M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems
• M. R. Garey, D. S. Johnson, Computers and Intractability, Problem LO5 (locator from secondary sources)
• C. H. Papadimitriou, Computational Complexity, Theorem 9.2 (locator from secondary sources)

structure Cslib.Complexity.MaxTwoSATInstance : Type

An instance (formula, target) of MAX 2-SAT.

• formula : Logic.PL.CNF ℕ

  The formula in conjunctive normal form, with at most two literals per clause.

• target : ℕ

  The minimum number of clauses that must be satisfied.

theorem Cslib.Complexity.MaxTwoSATInstance.ext {x y : MaxTwoSATInstance} (formula : x.formula = y.formula) (target : x.target = y.target) : x = y

theorem Cslib.Complexity.MaxTwoSATInstance.ext_iff {x y : MaxTwoSATInstance} : x = y ↔ x.formula = y.formula ∧ x.target = y.target

def Cslib.Complexity.instDecidableEqMaxTwoSATInstance.decEq (x✝ x✝¹ : MaxTwoSATInstance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Complexity.instDecidableEqMaxTwoSATInstance : DecidableEq MaxTwoSATInstance

@[instance_reducible]

instance Cslib.Complexity.instReprMaxTwoSATInstance : Repr MaxTwoSATInstance

def Cslib.Complexity.instReprMaxTwoSATInstance.repr : MaxTwoSATInstance → ℕ → Std.Format

@[simp]

theorem Cslib.Complexity.encMaxTwoSAT_apply (a : MaxTwoSATInstance) : encMaxTwoSAT a = encMaxTwoSATFields (a.formula, a.target)

theorem Cslib.Complexity.encMaxTwoSAT_target_inO : Turing.MultiTapeTM.ComputableInO MaxTwoSATInstance.target encMaxTwoSAT Turing.MultiTapeTM.encNat (fun (a : MaxTwoSATInstance) => (encMaxTwoSAT a).length) fun (a : MaxTwoSATInstance) => (encMaxTwoSAT a).length

theorem Cslib.Complexity.encMaxTwoSAT_formula_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MaxTwoSATInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMaxTwoSAT S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).formula) encIn✝ encCNF S✝

theorem Cslib.Complexity.encMaxTwoSAT_target_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MaxTwoSATInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMaxTwoSAT → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).target) encIn✝ Turing.MultiTapeTM.encNat

theorem Cslib.Complexity.encMaxTwoSAT_formula_polyTime {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {g✝ : γ✝ → MaxTwoSATInstance} : Turing.MultiTapeTM.ComputableInPolyTime g✝ encIn✝ encMaxTwoSAT → Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ✝) => (g✝ a).formula) encIn✝ encCNF

def Cslib.Complexity.encMaxTwoSAT : MaxTwoSATInstance ↪ List Bool

Encoding of MaxTwoSATInstance as (formula, target) with target in binary.

theorem Cslib.Complexity.encMaxTwoSAT_target_budget {γ✝ : Type} {encIn✝ : γ✝ ↪ List Bool} {S✝ : γ✝ → ℕ} {g✝ : γ✝ → MaxTwoSATInstance} : Turing.MultiTapeTM.ComputableInSpace g✝ encIn✝ encMaxTwoSAT S✝ → Turing.MultiTapeTM.ComputableInSpace (fun (a : γ✝) => (g✝ a).target) encIn✝ Turing.MultiTapeTM.encNat S✝

theorem Cslib.Complexity.encMaxTwoSAT_mk_inO {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CNF ℕ} {T0 S0 x1 T1 S1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInO x0 encIn encCNF T0 S0) (h1 : Turing.MultiTapeTM.ComputableInO x1 encIn Turing.MultiTapeTM.encNat T1 S1) : Turing.MultiTapeTM.ComputableInO (fun (x : γ) => { formula := x0 x, target := x1 x }) encIn encMaxTwoSAT (fun (x : γ) => T0 x + T1 x) fun (x : γ) => S0 x + S1 x

theorem Cslib.Complexity.encMaxTwoSAT_formula_deg : Turing.MultiTapeTM.ComputableInDegree MaxTwoSATInstance.formula encMaxTwoSAT encCNF 1 1

theorem Cslib.Complexity.encMaxTwoSAT_mk_budget {γ : Type} {encIn : γ ↪ List Bool} {budget : γ → ℕ} {x0 : γ → Logic.PL.CNF ℕ} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInSpace x0 encIn encCNF budget) (h1 : Turing.MultiTapeTM.ComputableInSpace x1 encIn Turing.MultiTapeTM.encNat budget) : Turing.MultiTapeTM.ComputableInSpace (fun (x : γ) => { formula := x0 x, target := x1 x }) encIn encMaxTwoSAT budget

theorem Cslib.Complexity.encMaxTwoSAT_mk_deg : Turing.MultiTapeTM.ComputableInDegree (fun (p : Logic.PL.CNF ℕ × ℕ) => { formula := p.1, target := p.2 }) encMaxTwoSATFields encMaxTwoSAT 1 1

theorem Cslib.Complexity.encMaxTwoSAT_fields_deg : Turing.MultiTapeTM.ComputableInDegree (fun (a : MaxTwoSATInstance) => (a.formula, a.target)) encMaxTwoSAT encMaxTwoSATFields 1 1

theorem Cslib.Complexity.encMaxTwoSAT_mk_polyTime {γ : Type} {encIn : γ ↪ List Bool} {x0 : γ → Logic.PL.CNF ℕ} {x1 : γ → ℕ} (h0 : Turing.MultiTapeTM.ComputableInPolyTime x0 encIn encCNF) (h1 : Turing.MultiTapeTM.ComputableInPolyTime x1 encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : γ) => { formula := x0 x, target := x1 x }) encIn encMaxTwoSAT

@[reducible, inline]

abbrev Cslib.Complexity.encMaxTwoSATFields : Logic.PL.CNF ℕ × ℕ ↪ List Bool

The tuple of the fields of encMaxTwoSAT.

theorem Cslib.Complexity.encMaxTwoSAT_target_deg : Turing.MultiTapeTM.ComputableInDegree MaxTwoSATInstance.target encMaxTwoSAT Turing.MultiTapeTM.encNat 1 1

theorem Cslib.Complexity.encMaxTwoSAT_formula_inO : Turing.MultiTapeTM.ComputableInO MaxTwoSATInstance.formula encMaxTwoSAT encCNF (fun (a : MaxTwoSATInstance) => (encMaxTwoSAT a).length) fun (a : MaxTwoSATInstance) => (encMaxTwoSAT a).length

def Cslib.Complexity.MaxTwoSAT : Set MaxTwoSATInstance

Maximum 2-satisfiability: the instances x : MaxTwoSATInstance such that every clause of x.formula has at most two literals and some assignment satisfies at least x.target clauses of x.formula, counted with multiplicity.

@[simp]

theorem Cslib.Complexity.mem_MaxTwoSAT_iff {φ : Logic.PL.CNF ℕ} {K : ℕ} : { formula := φ, target := K } ∈ MaxTwoSAT ↔ (∀ c ∈ φ, List.length c ≤ 2) ∧ ∃ (σ : ℕ → Bool), K ≤ List.countP (Logic.PL.Clause.eval σ) φ

Membership in MaxTwoSAT, unfolded.

Membership in NP

def Cslib.Complexity.MaxTwoSAT.verifier (x : MaxTwoSATInstance × List Bool) : Bool

The verifier for MaxTwoSAT: check that every clause has at most two literals and count the clauses satisfied by the certificate assignment of SAT.assignment.

theorem Cslib.Complexity.MaxTwoSAT.isVerifier : IsVerifier encMaxTwoSAT Polynomial.X verifier MaxTwoSAT

MaxTwoSAT.verifier verifies MaxTwoSAT with certificates as long as the encoded instance: the certificate lists the values of the variables in order of first occurrence.

theorem Cslib.Complexity.MaxTwoSAT.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encMaxTwoSAT Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Checking the clause widths and counting the satisfied clauses is polynomial-time: the count is computed in unary and compared with the binary target.

theorem Cslib.Complexity.MaxTwoSAT.mem_NP : MaxTwoSAT ∈ NP encMaxTwoSAT

MaxTwoSAT belongs to NP.

The gadget

def Cslib.Complexity.MaxTwoSAT.gadget (a b c : Logic.PL.Literal ℕ) (w : ℕ) : Logic.PL.CNF ℕ

The ten-clause gadget of Garey, Johnson and Stockmeyer for the clause a ∨ b ∨ c, with the variable w: the unit clauses a, b, c, w, the clauses ¬a ∨ ¬b, ¬a ∨ ¬c, ¬b ∨ ¬c, and the clauses a ∨ ¬w, b ∨ ¬w, c ∨ ¬w.

def Cslib.Complexity.MaxTwoSAT.gadgetScore (x y z q : Bool) : ℕ

The number of satisfied clauses of a gadget whose literals take the values x, y, z and whose variable takes the value q.

theorem Cslib.Complexity.MaxTwoSAT.countP_gadget (σ : ℕ → Bool) (a b c : Logic.PL.Literal ℕ) (w : ℕ) : List.countP (Logic.PL.Clause.eval σ) (gadget a b c w) = gadgetScore (Logic.PL.Literal.eval σ a) (Logic.PL.Literal.eval σ b) (Logic.PL.Literal.eval σ c) (σ w)

The number of satisfied clauses of a gadget depends only on the values of its literals and of its variable.

theorem Cslib.Complexity.MaxTwoSAT.gadgetScore_le (x y z q : Bool) : gadgetScore x y z q ≤ 7

A gadget never has more than seven satisfied clauses.

def Cslib.Complexity.MaxTwoSAT.majority (x y z : Bool) : Bool

The majority of three truth values.

theorem Cslib.Complexity.MaxTwoSAT.gadgetScore_majority {x y z : Bool} (h : (x || y || z) = true) : gadgetScore x y z (majority x y z) = 7

If the clause holds, setting the variable to the majority of its literals satisfies seven clauses of the gadget.

theorem Cslib.Complexity.MaxTwoSAT.gadgetScore_false_le (q : Bool) : gadgetScore false false false q ≤ 6

If the clause fails, the gadget has at most six satisfied clauses.

The reduction

def Cslib.Complexity.MaxTwoSAT.doubleLiteral (l : Logic.PL.Literal ℕ) : Logic.PL.Literal ℕ

Double the variable of a literal; the odd variables are then free for the gadgets.

def Cslib.Complexity.MaxTwoSAT.clauseGadget (c : Logic.PL.Clause ℕ) (i : ℕ) : Logic.PL.CNF ℕ

The gadget of the clause numbered i, whose first three literals are doubled, with the fresh variable 2 i + 1.

def Cslib.Complexity.toMaxTwoSAT (φ : Logic.PL.CNF ℕ) : MaxTwoSATInstance

The reduction from ExactThreeSAT to MaxTwoSAT: a formula all of whose clauses have three literals becomes the gadgets of its clauses, with target seven satisfied clauses per gadget. Any other formula becomes the formula with one empty clause and target one, a fixed no-instance: no assignment satisfies the empty clause.

theorem Cslib.Complexity.mem_MaxTwoSAT_toMaxTwoSAT_iff (φ : Logic.PL.CNF ℕ) : toMaxTwoSAT φ ∈ MaxTwoSAT ↔ φ ∈ ExactThreeSAT

A formula is in ExactThreeSAT exactly when its image under toMaxTwoSAT is in MaxTwoSAT.

Polynomial time

theorem Cslib.Complexity.computableInPolyTime_toMaxTwoSAT : Turing.MultiTapeTM.ComputableInPolyTime toMaxTwoSAT encCNF encMaxTwoSAT

The reduction toMaxTwoSAT is computable in polynomial time.

theorem Cslib.Complexity.polyTimeReducible_ExactThreeSAT_MaxTwoSAT : PolyTimeReducible encCNF encMaxTwoSAT ExactThreeSAT MaxTwoSAT

ExactThreeSAT reduces to MaxTwoSAT in polynomial time via toMaxTwoSAT.

theorem Cslib.Complexity.polyTimeReducible_ThreeSAT_MaxTwoSAT : PolyTimeReducible encCNF encMaxTwoSAT ThreeSAT MaxTwoSAT

ThreeSAT reduces to MaxTwoSAT in polynomial time: pad every clause to three literals by repetition (toExactThreeSAT), then apply toMaxTwoSAT.

theorem Cslib.Complexity.MaxTwoSAT_npHard : NPHard encMaxTwoSAT MaxTwoSAT

MaxTwoSAT is NP-hard.

theorem Cslib.Complexity.MaxTwoSAT_npComplete : NPComplete encMaxTwoSAT MaxTwoSAT

MAX 2-SAT is NP-complete Garey, Johnson and Stockmeyer (attribution from secondary sources). The target K is in binary, and clauses of one literal are allowed.