Minimum 2-satisfiability

AbbreviationMINIMUM 2-SATISFIABILITY instances#✓fully proved

An instance of MINIMUM 2-SATISFIABILITY 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). No condition is placed on \(\varphi\) here; clauses of at most two literals are required separately, by well-formedness.

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

Uses 1 · Used by 3

Statement usesCNF formula

Used byThe MINIMUM 2-SATISFIABILITY decision problem · Feasible MINIMUM 2-SATISFIABILITY instances · Well-formed MINIMUM 2-SATISFIABILITY instances

DefinitionWell-formed MINIMUM 2-SATISFIABILITY instances#✓fully proved

A triple \((n, \varphi, K)\) of a natural number \(n\), a CNF formula \(\varphi\) and a natural number \(K\) is well formed when every clause of \(\varphi\) has at most two literals and every literal of every clause has variable index less than \(n\).

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

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · MINIMUM 2-SATISFIABILITY instances

Used byThe MINIMUM 2-SATISFIABILITY decision problem

DefinitionFeasible MINIMUM 2-SATISFIABILITY instances#✓fully proved

A triple \((n, \varphi, K)\) of a natural number \(n\), a CNF formula \(\varphi\) with clauses \(C_0, \dots, C_{m-1}\) and a natural number \(K\) is feasible when there is an assignment of truth values to the variables \(0, \dots, n-1\) that, with every variable \(x \ge n\) set to false, satisfies \(C_j\) for at most \(K\) indices \(j < m\).

def MinTwoSatFeasible
    (i : MinTwoSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    ∃ S : Finset ℕ, S ⊆ Finset.range i.2.1.length ∧ S.card ≤ i.2.2 ∧
      ∀ j < i.2.1.length,
        Cslib.Logic.PL.CNFClause.Satisfies (fun x => assign.getD x false)
          (i.2.1.getD j []) ↔ j ∈ S

Uses 4 · Used by 1

Statement usesCNF formula · CNF clause · Satisfaction of a clause · MINIMUM 2-SATISFIABILITY instances

Used byThe MINIMUM 2-SATISFIABILITY decision problem

DefinitionThe MINIMUM 2-SATISFIABILITY decision problem#✓fully proved

MINIMUM 2-SATISFIABILITY is the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a triple \((n, \varphi, K)\) of a natural number \(n\), a CNF formula \(\varphi\) with clauses \(C_0, \dots, C_{m-1}\) and a natural number \(K\) such that every clause has at most two literals, all with variables less than \(n\), and some assignment of truth values to the variables \(0, \dots, n-1\) satisfies \(C_j\) for at most \(K\) indices \(j < m\). Every other bitstring is rejected.

noncomputable def minTwoSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MinTwoSatInstance) x with
  | some i => decide (WellFormed i ∧ MinTwoSatFeasible 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 MINIMUM 2-SATISFIABILITY instances · MINIMUM 2-SATISFIABILITY instances · Well-formed MINIMUM 2-SATISFIABILITY instances · Decision problems

Used byMINIMUM 2-SATISFIABILITY is NP-complete

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

Let MINIMUM 2-SATISFIABILITY be the decision problem that accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a triple \((n, \varphi, K)\) of a natural number \(n\), a CNF formula \(\varphi\) with clauses \(C_0, \dots, C_{m-1}\) and a natural number \(K\) such that every clause has at most two literals, all with variables less than \(n\), and some assignment of truth values to the variables \(0, \dots, n-1\) satisfies \(C_j\) for at most \(K\) indices \(j < m\). Then MINIMUM 2-SATISFIABILITY belongs to NP, and every decision problem \(L\) in NP reduces to it by a polynomial-time many-one reduction: there is a polynomial-time computable map \(f\) on bitstrings such that, for every bitstring \(x\), \(L\) accepts \(x\) exactly when MINIMUM 2-SATISFIABILITY accepts \(f(x)\).

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), MINIMUM 2-SATISFIABILITY; R. Kohli, R. Krishnamurti, and P. Mirchandani, "The minimum satisfiability problem" (1994).

Uses 5

Statement usesPolynomial-time many-one reduction · The MINIMUM 2-SATISFIABILITY 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.