3-SAT with bounded occurrences

AbbreviationBounded-occurrence 3-SAT instances#✓fully proved

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

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

Uses 1 · Used by 3

Statement usesCNF formula

Used by3-SAT with bounded occurrences as a decision problem · Satisfiable bounded-occurrence 3-SAT instances · Well-formed bounded-occurrence 3-SAT instances

DefinitionWell-formed bounded-occurrence 3-SAT instances#✓fully proved

A bounded-occurrence 3-SAT instance \((n, \varphi)\) is well formed when every clause of \(\varphi\) is a list of exactly three literals, not necessarily distinct, every literal of \(\varphi\) has a variable less than \(n\), and for every variable \(v < n\) at most four of the literals in the clauses of \(\varphi\), counted with multiplicity and with either polarity, have variable \(v\).

def WellFormed (i : BoundedOccurrenceThreeSatInstance) : Prop :=
  (∀ clause ∈ i.2, clause.length = 3 ∧ ∀ l ∈ clause, l.1 < i.1) ∧
    ∀ v < i.1, (i.2.flatten.filter (fun l => l.1 == v)).length ≤ 4

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · Bounded-occurrence 3-SAT instances

Used by3-SAT with bounded occurrences as a decision problem

DefinitionSatisfiable bounded-occurrence 3-SAT instances#✓fully proved

A bounded-occurrence 3-SAT instance \((n, \varphi)\) is satisfiable when there is a list \((a_0, \dots, a_{n-1})\) of booleans such that \(\varphi\) is satisfied by the assignment sending each variable \(x < n\) to \(a_x\) and every variable \(x \ge n\) to false.

def BoundedOccurrenceThreeSatFeasible
    (i : BoundedOccurrenceThreeSatInstance) : 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 · Bounded-occurrence 3-SAT instances

Used by3-SAT with bounded occurrences as a decision problem

Definition3-SAT with bounded occurrences as a decision problem#✓fully proved

The decision problem 3-SAT WITH BOUNDED OCCURRENCES accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of bounded-occurrence 3-SAT instances, to an instance that is well formed and satisfiable; it rejects every other bitstring, including every bitstring that does not decode.

noncomputable def boundedOccurrenceThreeSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := BoundedOccurrenceThreeSatInstance) x with
  | some i => decide (WellFormed i ∧ BoundedOccurrenceThreeSatFeasible 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 bounded-occurrence 3-SAT instances · Bounded-occurrence 3-SAT instances · Well-formed bounded-occurrence 3-SAT instances · Decision problems

Used by3-SAT WITH BOUNDED OCCURRENCES is NP-complete

Theorem3-SAT WITH BOUNDED OCCURRENCES is NP-complete#●ready to prove

The decision problem 3-SAT WITH BOUNDED OCCURRENCES over bitstrings belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), 3-SAT with bounded occurrences; C. A. Tovey, "A simplified NP-complete satisfiability problem" (1984).

Uses 5

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