1-in-3 SAT

Abbreviation1-in-3-SAT instances#✓fully proved

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

Any CNF formula is allowed here; that \(\varphi\) has three literals per clause, all over the variables below \(n\), is required separately by well-formedness.

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

Uses 1 · Used by 3

Statement usesCNF formula

Used byThe 1-in-3-SAT decision problem · Feasible 1-in-3-SAT instances · Well-formed 1-in-3-SAT instances

DefinitionWell-formed 1-in-3-SAT instances#✓fully proved

A 1-in-3-SAT instance \((n, \varphi)\) is well formed when every clause of \(\varphi\) has exactly three literals and every literal \((x, b)\) in it has variable index \(x < n\).

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

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · 1-in-3-SAT instances

Used byThe 1-in-3-SAT decision problem

DefinitionFeasible 1-in-3-SAT instances#✓fully proved

A 1-in-3-SAT instance \((n, \varphi)\) is feasible when there is an assignment \(v\) of truth values to the variables \(0, \dots, n - 1\), with variables \(y \ge n\) read as false, such that every clause of \(\varphi\) has exactly one position holding a literal \((y, b)\) with \(v(y) = b\).

def OneInThreeSatFeasible
    (i : OneInThreeSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    ∀ clause ∈ i.2, ∃ k < clause.length,
      Cslib.Logic.PL.CNFLiteral.Satisfies (fun x => assign.getD x false)
        (clause.getD k (0, false)) ∧
        ∀ j < clause.length,
          Cslib.Logic.PL.CNFLiteral.Satisfies (fun x => assign.getD x false)
            (clause.getD j (0, false)) → j = k

Uses 4 · Used by 1

Statement usesCNF formula · CNF clause · Satisfaction of a literal · 1-in-3-SAT instances

Used byThe 1-in-3-SAT decision problem

DefinitionThe 1-in-3-SAT decision problem#✓fully proved

The 1-in-3-SAT 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 clause of \(\varphi\) has exactly three literals, every literal \((y, b)\) of \(\varphi\) has variable index \(y < n\), and some assignment \(v\) of truth values to the variables \(0, \dots, n - 1\) makes exactly one position of every clause hold a literal \((y, b)\) with \(v(y) = b\). It rejects every bitstring that does not decode.

noncomputable def oneInThreeSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := OneInThreeSatInstance) x with
  | some i => decide (WellFormed i ∧ OneInThreeSatFeasible 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 1-in-3-SAT instances · 1-in-3-SAT instances · Well-formed 1-in-3-SAT instances · Decision problems

Used by1-IN-3-SAT is NP-complete

Theorem1-IN-3-SAT is NP-complete#●ready to prove

The 1-in-3-SAT decision problem belongs to NP, and every decision problem in NP reduces to it by a polynomial-time many-one reduction.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), ONE-IN-THREE 3-SAT; T. J. Schaefer, "The complexity of satisfiability problems" (1978).

Uses 5

Statement usesPolynomial-time many-one reduction · The 1-in-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.