Unsatisfiability

DefinitionUNSAT as a decision problem#✓fully proved

The UNSAT decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a pair \((n, \varphi)\) of a natural number \(n\) and a CNF formula \(\varphi\) such that every variable occurring in \(\varphi\) is less than \(n\) and, for every assignment \(a\) of booleans to the variables \(0, \dots, n - 1\), the assignment that agrees with \(a\) below \(n\) and sends every variable \(v \ge n\) to false does not satisfy \(\varphi\).

noncomputable def unsatDec : MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × Cslib.Logic.PL.CNF) x with
  | some i => decide ((∀ clause ∈ i.2, ∀ l ∈ clause, l.1 < i.1) ∧
      ∀ assign : Fin i.1 → Bool,
        ¬ Cslib.Logic.PL.CNF.Satisfies
          (fun v => if h : v < i.1 then assign ⟨v, h⟩ else false) i.2)
  | none => false

Uses 12 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF 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 · Decision problems

Used byUNSAT is coNP-complete

TheoremUNSAT is coNP-complete#●ready to prove

The UNSAT decision problem lies in coNP, and every decision problem in coNP has a polynomial-time many-one reduction to it.

public theorem_wanted unsat_conp_complete :
    unsatDec ∈ MetaMathlibExt.ComplexityTheory.coNP ∧
      ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
        L ∈ MetaMathlibExt.ComplexityTheory.coNP →
          Cslib.CookLevin.PolyManyOneRed L unsatDec

Sources

• S. A. Cook, "The complexity of theorem-proving procedures", Proceedings of the Third Annual ACM Symposium on Theory of Computing (STOC 1971), 151-158; L. A. Levin, "Universal search problems", Problems of Information Transmission 9 (1973), 265-266.

Uses 5

Statement usesPolynomial-time many-one reduction · UNSAT as a decision problem · Complexity classes · Decision problems · The class coNP

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.