Finite-domain constraint satisfaction problems and Boolean reduction

This module formalizes the canonical reduction from finite-domain constraint satisfaction problems (CSPs) over domain size q to Boolean CSPs. The finite-domain encoding is a standard extension (ruling out non-domain bit patterns with validity constraints) that builds on the Boolean subexponential counting framework of [OAI26c], Corollary C.2 / Theorem 1.1.

Each domain variable in a domain of size q is encoded by b = max 1 (Nat.clog 2 q) Boolean variables. Unused bit patterns in [q, 2^b) are ruled out by domain-validity constraints of scope length b for each declared variable v < N. Original constraints of arity r are translated to Boolean constraints of scope length r * b. When every constraint has arity at most k, the compiled Boolean CSP has constraint scope lengths bounded by max 1 k * b, and the number of satisfying assignments on declared variables is exactly preserved.

Main definitions

• Cslib.Logic.PL.CSP.bitWidth: the number of bits b = max 1 (Nat.clog 2 q) for domain q.
• Cslib.Logic.PL.CSP.bitScope: the list of b Boolean variables representing domain variable v.
• Cslib.Logic.PL.CSP.decodeChunks: extract decoded natural numbers from chunked bit lists.
• Cslib.Logic.PL.CSP.toFin: clamped conversion of natural numbers into Fin q.
• Cslib.Logic.PL.CSP.semBoolean: the Boolean semantics evaluating domain-validity (none) and original relation (some R) constraints.
• Cslib.Logic.PL.CSP.toBoolean: compilation of a finite-domain CSP on declared variables 0, …, N - 1 into an equivalent Boolean CSP.

Main results

• Cslib.Logic.PL.CSP.all_length_le_toBoolean: constraint scope length bound max 1 k * bitWidth q.
• Cslib.Logic.PL.CSP.vars_toBoolean_subset, Cslib.Logic.PL.CSP.numVars_toBoolean_le: all variables bounded by N * bitWidth q.
• Cslib.Logic.PL.CSP.validDeclaredCSP_toBoolean: validity of compiled Boolean CSP on declared variables.
• Cslib.Logic.PL.CSP.modelCountOn_toBoolean, Cslib.Logic.PL.CSP.satisfiable_toBoolean: exact equality of declared-variable model counts and satisfiability equivalence between the finite-domain CSP and its Boolean compilation.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix C.2, Corollary C.2.

Binary encoding and conversions

def Cslib.Logic.PL.CSP.bitWidth (q : ℕ) : ℕ

The number of bits needed to encode a domain of size q. Always at least 1.

theorem Cslib.Logic.PL.CSP.one_le_bitWidth (q : ℕ) : 1 ≤ bitWidth q

bitWidth q is always at least 1.

theorem Cslib.Logic.PL.CSP.le_two_pow_bitWidth (q : ℕ) : q ≤ 2 ^ bitWidth q

q is at most 2 ^ bitWidth q.

def Cslib.Logic.PL.CSP.bitScope (b v : ℕ) : List ℕ

The b Boolean variables representing domain variable v.

@[simp]

theorem Cslib.Logic.PL.CSP.bitScope_length (b v : ℕ) : (bitScope b v).length = b

theorem Cslib.Logic.PL.CSP.mem_bitScope_iff (b v x : ℕ) : x ∈ bitScope b v ↔ ∃ j < b, x = v * b + j

theorem Cslib.Logic.PL.CSP.bitScope_subset_range {b v N : ℕ} (hv : v < N) (x : ℕ) : x ∈ bitScope b v → x < N * b

def Cslib.Logic.PL.CSP.decodeChunks (b : ℕ) : ℕ → List Bool → List ℕ

Decode a list of bits into r natural numbers by taking successive chunks of width b.

@[simp]

theorem Cslib.Logic.PL.CSP.decodeChunks_zero (b : ℕ) (bs : List Bool) : decodeChunks b 0 bs = []

@[simp]

theorem Cslib.Logic.PL.CSP.decodeChunks_length (b r : ℕ) (bs : List Bool) : (decodeChunks b r bs).length = r

theorem Cslib.Logic.PL.CSP.decodeChunks_flatMap (b : ℕ) {α : Type u_2} (vs : List α) (f : α → List Bool) (hf : ∀ v ∈ vs, (f v).length = b) : decodeChunks b vs.length (List.flatMap f vs) = List.map (BitString.lsbValue ∘ f) vs

def Cslib.Logic.PL.CSP.toFin (q : ℕ) (hq : 0 < q) (x : ℕ) : Fin q

Clamped conversion from natural numbers into Fin q.

@[simp]

theorem Cslib.Logic.PL.CSP.toFin_val_of_lt {q : ℕ} (hq : 0 < q) {x : ℕ} (h : x < q) : ↑(toFin q hq x) = x

@[simp]

theorem Cslib.Logic.PL.CSP.toFin_of_val {q : ℕ} (hq : 0 < q) (x : Fin q) : toFin q hq ↑x = x

Boolean reduction for finite-domain CSP

def Cslib.Logic.PL.CSP.semBoolean {Rel : Type u_1} (q : ℕ) (sem : Rel → List (Fin q) → Bool) : Option Rel → List Bool → Bool

Boolean semantics for compiled finite-domain constraints:

• none: domain-validity constraint asserting length b and lsbValue bs < q.
• some R: relation constraint decoding bs into $r$ chunks of length b and evaluating sem R.

def Cslib.Logic.PL.CSP.toBoolean {Rel : Type u_1} (q N : ℕ) (F : CSP Rel ℕ) : CSP (Option Rel) ℕ

Compile a finite-domain CSP on declared variables 0, …, N - 1 into an equivalent Boolean CSP. Emits a domain-validity constraint (none, bitScope b v) for every v < N, and translates each constraint (R, vs) to (some R, vs.flatMap (bitScope b)).

theorem Cslib.Logic.PL.CSP.all_length_le_toBoolean {Rel : Type u_1} {k q N : ℕ} {F : CSP Rel ℕ} (hF : ∀ c ∈ F, c.2.length ≤ k) (c : Constraint (Option Rel) ℕ) : c ∈ toBoolean q N F → c.2.length ≤ max 1 k * bitWidth q

The constraint scope length of every clause in the compiled Boolean CSP is bounded by max 1 k * bitWidth q.

theorem Cslib.Logic.PL.CSP.vars_toBoolean_subset {Rel : Type u_1} {q N : ℕ} {F : CSP Rel ℕ} (hvars : ∀ v ∈ F.vars, v < N) (x : ℕ) : x ∈ (toBoolean q N F).vars → x < N * bitWidth q

All variables in the compiled Boolean CSP are strictly bounded by N * bitWidth q.

theorem Cslib.Logic.PL.CSP.validDeclaredCSP_toBoolean {Rel : Type u_1} {k q N : ℕ} {F : CSP Rel ℕ} (hw : ∀ c ∈ F, c.2.length ≤ k) (hvars : ∀ v ∈ F.vars, v < N) : validDeclaredCSP (max 1 k * bitWidth q) (N * bitWidth q) (toBoolean q N F) = true

The compiled Boolean CSP satisfies validDeclaredCSP with width max 1 k * bitWidth q and variable bound N * bitWidth q.

Model count equivalence

theorem Cslib.Logic.PL.CSP.modelCountOn_toBoolean {Rel : Type u_1} (q : ℕ) [Inhabited (Fin q)] (N : ℕ) (sem : Rel → List (Fin q) → Bool) (F : CSP Rel ℕ) (hvars : ∀ v ∈ F.vars, v < N) : modelCountOn (semBoolean q sem) (toBoolean q N F) (Finset.range (N * bitWidth q)) = modelCountOn sem F (Finset.range N)

Count-preserving bijection for finite-domain CSP to Boolean CSP. The declared-variable model count of a finite-domain CSP on 0, …, N - 1 equals the declared-variable model count of its compiled Boolean CSP on 0, …, N * bitWidth q - 1.

theorem Cslib.Logic.PL.CSP.numVars_toBoolean_le {Rel : Type u_1} {q N : ℕ} {F : CSP Rel ℕ} (hvars : ∀ v ∈ F.vars, v < N) : (toBoolean q N F).numVars ≤ N * bitWidth q

The number of distinct occurring variables in F.toBoolean q N is at most N * CSP.bitWidth q.

@[simp]

theorem Cslib.Logic.PL.CSP.satisfiable_toBoolean {Rel : Type u_1} (q : ℕ) [Inhabited (Fin q)] (N : ℕ) (sem : Rel → List (Fin q) → Bool) (F : CSP Rel ℕ) (hvars : ∀ v ∈ F.vars, v < N) : Satisfiable (semBoolean q sem) (toBoolean q N F) ↔ Satisfiable sem F

F.toBoolean q N is satisfiable under CSP.semBoolean q sem if and only if F is satisfiable under sem, whenever all occurring variables of F are < N.