Maximum 2-satisfiability

AbbreviationMAX-2SAT instances#✓fully proved

A MAX-2SAT instance is a triple \((n, \varphi, K)\) of a natural number \(n\) (the number of variables), a CNF formula \(\varphi\) and a natural number \(K\) (the bound). The type does not restrict clause lengths; that clauses have at most two literals is part of well-formedness.

abbrev MaxTwoSatInstance := ℕ × Cslib.Logic.PL.CNF × ℕ

Uses 1 · Used by 3

Statement usesCNF formula

Used byMAXIMUM 2-SATISFIABILITY as a decision problem · Feasible MAX-2SAT instances · Well-formed MAX-2SAT instances

DefinitionWell-formed MAX-2SAT instances#✓fully proved

A MAX-2SAT instance \((n, \varphi, K)\) is well formed when every clause of \(\varphi\) has at most two literals and every literal \((x, b)\) in it has variable index \(x < n\).

def WellFormed (i : MaxTwoSatInstance) : Prop :=
  (∀ clause ∈ i.2.1, clause.length ≤ 2 ∧ ∀ l ∈ clause, l.1 < i.1)

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · MAX-2SAT instances

Used byMAXIMUM 2-SATISFIABILITY as a decision problem

DefinitionFeasible MAX-2SAT instances#✓fully proved

A MAX-2SAT instance \((n, \varphi, K)\) is feasible when there are truth values \(a_0, \dots, a_{n-1}\) such that at least \(K\) of the clauses in the list \(\varphi\), counted with multiplicity, are satisfied by the assignment \(v\) with \(v(x) = a_x\) for \(x < n\) and \(v(x) = \mathrm{false}\) for \(x \ge n\).

def MaxTwoSatFeasible
    (i : MaxTwoSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    ∃ sub : Cslib.Logic.PL.CNF, sub.Sublist i.2.1 ∧ i.2.2 ≤ sub.length ∧
      ∀ clause ∈ sub, Cslib.Logic.PL.CNFClause.Satisfies
        (fun x => assign.getD x false) clause

Uses 4 · Used by 1

Statement usesCNF formula · CNF clause · Satisfaction of a clause · MAX-2SAT instances

Used byMAXIMUM 2-SATISFIABILITY as a decision problem

DefinitionMAXIMUM 2-SATISFIABILITY as a decision problem#✓fully proved

The decision problem MAXIMUM 2-SATISFIABILITY accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of MAX-2SAT instances, to an instance \((n, \varphi, K)\) that is well formed (every clause of \(\varphi\) has at most two literals, and every literal has variable index less than \(n\)) and feasible (some assignment of truth values to the \(n\) variables satisfies at least \(K\) of the clauses of \(\varphi\), counted with multiplicity). Bitstrings that do not decode, and bitstrings that decode to instances that are not well formed, are rejected.

noncomputable def maxTwoSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaxTwoSatInstance) x with
  | some i => decide (WellFormed i ∧ MaxTwoSatFeasible i)
  | none => false

Uses 14 · Used by 1

Statement usesCNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Feasible MAX-2SAT instances · MAX-2SAT instances · Well-formed MAX-2SAT instances · Decision problems

Used byMAXIMUM 2-SATISFIABILITY is NP-complete

TheoremMAXIMUM 2-SATISFIABILITY is NP-complete#●ready to prove

The decision problem MAXIMUM 2-SATISFIABILITY over bitstrings lies in NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

public theorem_wanted maxTwoSat_npComplete :
    maxTwoSatDec ∈ MetaMathlibExt.ComplexityTheory.NP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.NP →
          Cslib.CookLevin.PolyManyOneRed L maxTwoSatDec

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), MAXIMUM 2-SATISFIABILITY.

Uses 5

Statement usesPolynomial-time many-one reduction · MAXIMUM 2-SATISFIABILITY as a decision problem · Complexity classes · Decision problems · The complexity class NP

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.