Not-all-equal 3-SAT

AbbreviationNOT-ALL-EQUAL 3-SAT instances#✓fully proved

A NOT-ALL-EQUAL 3-SAT instance is a pair \((n, \varphi)\) of a natural number \(n\), the number of variables, and a CNF formula \(\varphi\). The formula is not required to have three literals per clause; that is part of well-formedness.

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

Uses 1 · Used by 3

Statement usesCNF formula

Used byNOT-ALL-EQUAL 3-SAT as a decision problem · Not-all-equal satisfiability of an instance · Well-formed NOT-ALL-EQUAL 3-SAT instances

DefinitionWell-formed NOT-ALL-EQUAL 3-SAT instances#✓fully proved

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

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

Uses 3 · Used by 1

Statement usesCNF formula · CNF clause · NOT-ALL-EQUAL 3-SAT instances

Used byNOT-ALL-EQUAL 3-SAT as a decision problem

DefinitionNot-all-equal satisfiability of an instance#✓fully proved

A NOT-ALL-EQUAL 3-SAT instance \((n, \varphi)\), with \(n \in \mathbb{N}\) and \(\varphi\) a CNF formula, is not-all-equal satisfiable when there are truth values \(a_0, \dots, a_{n-1}\) such that, for the assignment \(v\) with \(v(x) = a_x\) for \(x < n\) and \(v(x) = \mathrm{false}\) for \(x \ge n\), every clause of \(\varphi\) contains a literal satisfied by \(v\) and a literal not satisfied by \(v\).

def NaeThreeSatFeasible
    (i : NaeThreeSatInstance) : Prop :=
  ∃ assign : List Bool, assign.length = i.1 ∧
    ∀ clause ∈ i.2, Cslib.Logic.PL.CNFClause.Satisfies (fun x => assign.getD x false) clause ∧
      ∃ l ∈ clause, ¬ Cslib.Logic.PL.CNFLiteral.Satisfies (fun x => assign.getD x false) l

Uses 5 · Used by 1

Statement usesCNF formula · CNF clause · Satisfaction of a clause · Satisfaction of a literal · NOT-ALL-EQUAL 3-SAT instances

Used byNOT-ALL-EQUAL 3-SAT as a decision problem

DefinitionNOT-ALL-EQUAL 3-SAT as a decision problem#✓fully proved

The decision problem NOT-ALL-EQUAL 3-SAT accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a NOT-ALL-EQUAL 3-SAT instance \((n, \varphi)\) that is well-formed and not-all-equal satisfiable. Every bitstring that decodes to no instance is rejected.

noncomputable def naeThreeSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := NaeThreeSatInstance) x with
  | some i => decide (WellFormed i ∧ NaeThreeSatFeasible 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 · Not-all-equal satisfiability of an instance · NOT-ALL-EQUAL 3-SAT instances · Well-formed NOT-ALL-EQUAL 3-SAT instances · Decision problems

Used byNOT-ALL-EQUAL 3-SAT is NP-complete

TheoremNOT-ALL-EQUAL 3-SAT is NP-complete#●ready to prove

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

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

Sources

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

Uses 5

Statement usesPolynomial-time many-one reduction · NOT-ALL-EQUAL 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.