Monotone 3-SAT

AbbreviationMonotone 3-SAT instances#✓fully proved

A monotone 3-SAT instance is a pair \((n, \varphi)\) of a natural number \(n\), the number of variables, and a CNF formula \(\varphi\).

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

Uses 1 · Used by 3

Statement usesCNF formula

Used byMONOTONE 3-SAT as a decision problem · Satisfiable monotone 3-SAT instances · Well-formed monotone 3-SAT instances

DefinitionWell-formed monotone 3-SAT instances#✓fully proved

A monotone 3-SAT instance \((n, \varphi)\) is well formed when every clause of the CNF formula \(\varphi\) is a list of exactly three literals (repetitions allowed), each with a variable below \(n\), and the literals of each clause are all positive or all negative.

def WellFormed (i : MonotoneThreeSatInstance) : Prop :=
  (∀ clause ∈ i.2, clause.length = 3 ∧ (∀ l ∈ clause, l.1 < i.1) ∧
    ((∀ l ∈ clause, l.2 = true) ∨ (∀ l ∈ clause, l.2 = false)))

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · Monotone 3-SAT instances

Used byMONOTONE 3-SAT as a decision problem

DefinitionSatisfiable monotone 3-SAT instances#✓fully proved

A monotone 3-SAT instance \((n, \varphi)\) is feasible when there is a list of \(n\) truth values \(a_0, \dots, a_{n-1}\) such that the assignment sending each variable \(x < n\) to \(a_x\) and every variable \(x \ge n\) to false satisfies the CNF formula \(\varphi\).

def MonotoneThreeSatFeasible
    (i : MonotoneThreeSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    Cslib.Logic.PL.CNF.Satisfies (fun x => assign.getD x false) i.2

Uses 3 · Used by 1

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

Used byMONOTONE 3-SAT as a decision problem

DefinitionMONOTONE 3-SAT as a decision problem#✓fully proved

The decision problem MONOTONE 3-SAT 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 clause of \(\varphi\) is a list of exactly three literals (repetitions allowed), every literal of \(\varphi\) has a variable below \(n\), the literals of each clause are all positive or all negative, and some assignment of truth values to the variables \(0, \dots, n-1\), with every other variable false, satisfies \(\varphi\). Bitstrings that do not decode are rejected.

noncomputable def monotoneThreeSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := MonotoneThreeSatInstance) x with
  | some i => decide (WellFormed i ∧ MonotoneThreeSatFeasible 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 · Satisfiable monotone 3-SAT instances · Monotone 3-SAT instances · Well-formed monotone 3-SAT instances · Decision problems

Used byMONOTONE 3-SAT is NP-complete

TheoremMONOTONE 3-SAT is NP-complete#●ready to prove

The decision problem MONOTONE 3-SAT belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to MONOTONE 3-SAT.

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

Sources

• T. J. Schaefer, "The complexity of satisfiability problems", Proceedings of the Tenth Annual ACM Symposium on Theory of Computing (STOC 1978), ACM, 1978, 216-226 (dichotomy theorem).

Uses 5

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