Binary constraint satisfaction

AbbreviationBinary CSP instances#✓fully proved

A binary CSP instance is a pair consisting of a list \((D_0, \dots, D_{n-1})\) of lists of natural numbers, where \(D_j\) is the domain of variable \(j\), and a list of constraints, each a triple \((j, k, P)\) of two variable indices \(j, k \in \mathbb{N}\) and a list \(P\) of allowed value pairs in \(\mathbb{N} \times \mathbb{N}\).

abbrev BinaryCspInstance := List (List ℕ) × List (ℕ × ℕ × List (ℕ × ℕ))

Used by 3

Used byBinary constraint satisfaction as a decision problem · Feasible binary CSP instances · Well-formed binary CSP instances

DefinitionWell-formed binary CSP instances#✓fully proved

A binary CSP instance with domain list \((D_0, \dots, D_{n-1})\) and constraint list \(C\) is well formed when every constraint \((j, k, P) \in C\) has \(j < n\) and \(k < n\).

def WellFormed (i : BinaryCspInstance) : Prop :=
  (∀ c ∈ i.2, c.1 < i.1.length ∧ c.2.1 < i.1.length)

Uses 1 · Used by 1

Statement usesBinary CSP instances

Used byBinary constraint satisfaction as a decision problem

DefinitionFeasible binary CSP instances#✓fully proved

A binary CSP instance with domain list \((D_0, \dots, D_{n-1})\) and constraint list \(C\) is feasible when there is a list \((a_0, \dots, a_{n-1})\) of natural numbers with \(a_j \in D_j\) for every \(j < n\) and \((a_j, a_k) \in P\) for every constraint \((j, k, P) \in C\), where \(a_i\) is read as \(0\) for every index \(i \ge n\).

def BinaryCspFeasible
    (i : BinaryCspInstance) : Prop :=
  ∃ assign : List ℕ, assign.length = i.1.length ∧
    (∀ d < i.1.length, assign.getD d 0 ∈ i.1.getD d []) ∧
    ∀ c ∈ i.2, (assign.getD c.1 0, assign.getD c.2.1 0) ∈ c.2.2

Uses 1 · Used by 1

Statement usesBinary CSP instances

Used byBinary constraint satisfaction as a decision problem

DefinitionBinary constraint satisfaction as a decision problem#✓fully proved

The decision problem BINARY CONSTRAINT SATISFACTION accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of binary CSP instances, to an instance that is well formed and feasible; it rejects every other bitstring, including every bitstring that does not decode.

noncomputable def binaryCspDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := BinaryCspInstance) x with
  | some i => decide (WellFormed i ∧ BinaryCspFeasible i)
  | none => false

Uses 12 · Used by 1

Statement usesBitstring 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 binary CSP instances · Binary CSP instances · Well-formed binary CSP instances · Decision problems

Used byBINARY CONSTRAINT SATISFACTION is NP-complete

TheoremBINARY CONSTRAINT SATISFACTION is NP-complete#●ready to prove

The decision problem BINARY CONSTRAINT SATISFACTION over bitstrings belongs to NP, and every decision problem in NP has a polynomial-time many-one reduction to it.

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

Sources

• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness (1979), CONSTRAINT SATISFACTION; R. Dechter, Constraint Processing (2003).

Uses 5

Statement usesPolynomial-time many-one reduction · Binary constraint satisfaction 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.