Maximum satisfiability

AbbreviationMAX-SAT instances#✓fully proved

A MAX-SAT 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).

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

Uses 1 · Used by 3

Statement usesCNF formula

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

DefinitionWell-formed MAX-SAT instances#✓fully proved

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

def WellFormed (i : MaxSatInstance) : Prop :=
  (∀ clause ∈ i.2.1, ∀ l ∈ clause, l.1 < i.1)

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · MAX-SAT instances

Used byMAXIMUM SATISFIABILITY as a decision problem

DefinitionFeasible MAX-SAT instances#✓fully proved

A MAX-SAT 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 MaxSatFeasible
    (i : MaxSatInstance) : 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-SAT instances

Used byMAXIMUM SATISFIABILITY as a decision problem

DefinitionMAXIMUM SATISFIABILITY as a decision problem#✓fully proved

The decision problem MAXIMUM SATISFIABILITY accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of MAX-SAT instances, to an instance \((n, \varphi, K)\) that is well formed (every literal of \(\varphi\) 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 maxSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MaxSatInstance) x with
  | some i => decide (WellFormed i ∧ MaxSatFeasible 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-SAT instances · MAX-SAT instances · Well-formed MAX-SAT instances · Decision problems

Used byMAXIMUM SATISFIABILITY is NP-complete

TheoremMAXIMUM SATISFIABILITY is NP-complete#●ready to prove

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

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · MAXIMUM 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.