Minimum-ones 3-SAT

AbbreviationMINIMUM ONES 3-SAT instances#✓fully proved

An instance of MINIMUM ONES 3-SAT 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 exactly three literals are required separately, by well-formedness.

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

Uses 1 · Used by 3

Statement usesCNF formula

Used byThe MINIMUM ONES 3-SAT decision problem · Feasible MINIMUM ONES 3-SAT instances · Well-formed MINIMUM ONES 3-SAT instances

DefinitionWell-formed MINIMUM ONES 3-SAT 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\) is a list of exactly three literals and every literal of every clause has variable index less than \(n\).

def WellFormed (i : MinOnesThreeSatInstance) : Prop :=
  (∀ clause ∈ i.2.1, clause.length = 3 ∧ ∀ l ∈ clause, l.1 < i.1)

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · MINIMUM ONES 3-SAT instances

Used byThe MINIMUM ONES 3-SAT decision problem

DefinitionFeasible MINIMUM ONES 3-SAT instances#✓fully proved

A triple \((n, \varphi, K)\) of a natural number \(n\), a CNF formula \(\varphi\) 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 \(\varphi\) and sets at most \(K\) of the variables \(0, \dots, n-1\) to true.

def MinOnesThreeSatFeasible
    (i : MinOnesThreeSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    (Cslib.Logic.PL.CNF.Satisfies (fun x => assign.getD x false) i.2.1) ∧
    (assign.filter (fun b => b)).length ≤ i.2.2

Uses 3 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · MINIMUM ONES 3-SAT instances

Used byThe MINIMUM ONES 3-SAT decision problem

DefinitionThe MINIMUM ONES 3-SAT decision problem#✓fully proved

MINIMUM ONES 3-SAT 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\) and a natural number \(K\) such that every clause of \(\varphi\) is a list of exactly three literals whose variables are all less than \(n\), and some assignment of truth values to the variables \(0, \dots, n-1\) satisfies \(\varphi\) and sets at most \(K\) of them to true. Every other bitstring is rejected.

noncomputable def minOnesThreeSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MinOnesThreeSatInstance) x with
  | some i => decide (WellFormed i ∧ MinOnesThreeSatFeasible 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 ONES 3-SAT instances · MINIMUM ONES 3-SAT instances · Well-formed MINIMUM ONES 3-SAT instances · Decision problems

Used byMINIMUM ONES 3-SAT is NP-complete

TheoremMINIMUM ONES 3-SAT is NP-complete#●ready to prove

Let MINIMUM ONES 3-SAT 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\) and a natural number \(K\) such that every clause of \(\varphi\) is a list of exactly three literals whose variables are all less than \(n\), and some assignment of truth values to the variables \(0, \dots, n-1\) satisfies \(\varphi\) and sets at most \(K\) of them to true. Then MINIMUM ONES 3-SAT 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 ONES 3-SAT accepts \(f(x)\).

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · The MINIMUM ONES 3-SAT 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.