Skip to content

Setoid.Complexity.CSP

Constraint Satisfaction Problems

This is the Setoid.Complexity.CSP module of the Agda Universal Algebra Library.

This module is the canonical home for the content previously developed in Legacy.Base.Complexity.CSP, ported under #307 (M2-7c). The relational formulation of CSP and the Galois connection to polymorphism clones (Jeavons) are stated below; substantive theorems β€” most importantly the Jeavons Galois connection itself for a fixed finite domain, and a statement of the Bulatov–Zhuk algebraic dichotomy β€” are scheduled under #274 (M7-1). The infinite-template / Ο‰-categorical extension is covered separately under #281 (M9-2), which depends on this canonical-path version.

The relational formulation of CSP

Let π’œ = (𝐴 , 𝑅ᡃ) be a relational structure (or 𝑅-structure), that is, a pair consisting of a set 𝐴 along with a collection 𝑅ᡃ βŠ† ⋃ₙ 𝒫(𝐴ⁿ) of relations on 𝐴.

We associate with π’œ a constraint satisfaction problem denoted by CSP(π’œ), which is the decision problem that is solved by finding an algorithm or program that does the following:

Take as input

  • an instance, which is an 𝑅-structure ℬ = (𝐡 , 𝑅ᡇ) (in the same signature as π’œ)

Output

  • "yes" or "no" according as there is, or is not, a solution, which is a 𝑅-structure homomorphism h : ℬ β†’ π’œ.

If there is such an algorithm that takes at most a power of 𝑛 operations to process an input structure ℬ of size 𝑛 (i.e., 𝑛 bits of memory are required to encode ℬ), then we say that CSP(π’œ) is tractable. Otherwise, CSP(π’œ) is intractable.

Equivalently, if we define

CSP(π’œ) := { ℬ ∣ ℬ an 𝑅-structure and βˆƒ hom ℬ β†’ π’œ }

then the CSP problem described above is simply the membership problem for the subset CSP(π’œ) of 𝑅 structures having homomorphisms into π’œ. That is, our algorithm must take as input an 𝑅-structure (a relational structure in the signature of π’œ) and decide whether or not it belongs to the set CSP(π’œ).

Connection to algebraic CSP

Let A be a set, let Op(A) denote the set of all operations, Rel(A) the set of all relations, on A.

Given R βŠ† Rel(A), define the set of operations on A that preserve all relations in R as follows:

∣: βƒ– R = { f ∈ Op(𝐴) ∣ βˆ€ r ∈ R, f ∣: r }.

Recall, f ∣: r is our notation for f Preserves r ⟢ r, which means that r is a subuniverse of a power of the algebra (A , {f}). Equivalently, f Preserves r ⟢ r means the following: if f is π‘š-ary and r is 𝑛-ary, then for every size-π‘š collection π‘Žπ‘  of 𝑛-tuples from r (that is, ∣ π‘Žπ‘  ∣ = π‘š and βˆ€ a ∈ π‘Žπ‘ , r a) we have r (f ∘ (zip π‘Žπ‘ )).

If π’œ = (A , R) is a relational structure, then the set ∣: βƒ–R of operations on A that preserve all relations in R is called the set of polymorphisms of π’œ.

Conversely, starting with a collection F βŠ† Op(A) of operations on A, define the set of all relations preserved by the functions in F as follows:

F βƒ— ∣: = { r ∈ Rel(A) ∣ βˆ€ f ∈ F, f ∣: r }.

It is easy to see that for all F βŠ† Op(A) and all R βŠ† Rel(A), we have

F βŠ† ∣: βƒ– (F βƒ— ∣:) and R βŠ† (∣: βƒ– R) βƒ— ∣:.

Let 𝑨(R) denote the algebraic structure with domain A and operations ∣: βƒ– R. Then every r ∈ R is a subalgebra of a power of 𝑨(R). Clearly (∣: βƒ– R) βƒ— ∣: is the set 𝖲 (𝖯fin 𝑨(R)) of subalgebras of finite powers of 𝑨(R).

The reason this Galois connection is useful is due to the following fact (observed by Peter Jeavons in the late 1990's):

Theorem. Let π’œ = (A, R) be a finite relational structure. If R' βŠ† (∣: βƒ– R) βƒ— ∣: is finite, then CSP((A, R')) is reducible in poly-time to CSP(π’œ)

In particular, the tractability of CSP(π’œ) depends only on its associated polymorphism algebra, 𝑨(R) := (A , ∣: βƒ– R).

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module Setoid.Complexity.CSP where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library ---------------------------------------
open import Function.Base    using ( _∘_ )
open import Level            using ( _βŠ”_ ; Level ) renaming ( suc to lsuc )
open import Relation.Binary  using ( Setoid )

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Overture                     using ( π“ž ; π“₯ ; Signature )
open import Setoid.Relations.Continuous  using ( REL-syntax )
open import Setoid.Algebras.Basic        using ( Algebra ; 𝔻[_] ; π•Œ[_] )

Constraints

A constraint c consists of

  1. a scope function, s : I β†’ var, and
  2. a constraint relation, i.e., a predicate over the function type I β†’ D
    I Β·Β·Β·> var
 .     .
  .   .
   ⌟ ⌞
    D

The scope of a constraint is an indexed subset of the set of variable symbols. We could define a type for this, e.g.,

Scope : Type Ξ½ β†’ Type ΞΉ β†’ _
Scope V I = I β†’ V

but we omit this definition because it's so simple; to reiterate, a scope of "arity" I on "variables" V is simply a map from I to V, where,

  • I denotes the "number" of variables involved in the scope
  • V denotes a collection (type) of "variable symbols"
module  _        -- levels for...
  {ΞΉ : Level}    -- ...arity (or argument index) types
  {Ξ½ : Level}    -- ...variable symbol types
  {α ρ : Level}  -- ...domain carrier and equivalence levels
  {ρʳ : Level}   -- ...constraint relation level
  where
  open Setoid using (Carrier)

  record Constraint (var : Type Ξ½) (dom : var β†’ Setoid Ξ± ρ)
                    : Type (Ξ½ βŠ” Ξ± βŠ” lsuc (ΞΉ βŠ” ρʳ)) where
    field
      arity  : Type ΞΉ               -- the cardinality of the set of constraint variables;
      scope  : arity β†’ var          -- which variables are involved in the constraint;
      rel    : REL[ i ∈ arity ] dom (scope i) .Carrier -- the constraint relation.

    satisfies : (βˆ€ v β†’ dom v .Carrier) β†’ Type ρʳ  -- An assignment, 𝑓 : var β†’ dom, of values to variables
    satisfies f = rel (f ∘ scope)                 -- *satisfies* the constraint 𝐢 = (Οƒ , 𝑅) provided
                                                  -- 𝑓 ∘ Οƒ ∈ 𝑅, where Οƒ is the scope of the constraint.
  open Constraint

Note on ρʳ. The constraint-relation level ρʳ is fixed at the module level rather than parameterizing each Constraint independently. This matches the universal-algebraic CSP literature, where every constraint of an instance typically lives at the same relation level (in practice 0β„“). Lifting ρʳ to a per-record parameter is a mechanical refactor that may become warranted when later content (e.g., the M7-1 polymorphism-clone development under #274 or the M9-2 infinitary CSP work under #281) needs to mix relation levels across constraints in a single instance.

CSP templates and instances

A CSP "template" restricts the relations that may occur in instances of the problem. A convenient way to specify a template is to give an indexed family π’œ : var β†’ Algebra Ξ± ρ of algebras (one for each variable symbol in var) and require that relations be subalgebras of the product β¨… var π’œ.

To construct a CSP instance, then, we just have to give a family π’œ of algebras, specify the number (ar) of constraints, and for each i : ar, define a constraint as a relation over (some of) the members of π’œ.

An instance of a constraint satisfaction problem is a triple 𝑃 = (𝑉, 𝐷, 𝐢) where * 𝑉 denotes a set of "variables" * 𝐷 denotes a "domain", * 𝐢 denotes an indexed collection of constraints.

  record CSPInstance (var : Type Ξ½) {𝑆 : Signature π“ž π“₯} (π’œ : var β†’ Algebra {𝑆 = 𝑆} Ξ± ρ)
    : Type (Ξ± βŠ” Ξ½ βŠ” lsuc (ΞΉ βŠ” ρʳ)) where
    field
      ar : Type ΞΉ   -- index on the constraints in the instance
      cs : (i : ar) β†’ Constraint var Ξ» v β†’ 𝔻[ π’œ v ]

    isSolution : (βˆ€ v β†’ π•Œ[ π’œ v ]) β†’ Type (ΞΉ βŠ” ρʳ)  -- An assignment *solves* the instance
    isSolution f = βˆ€ i β†’ satisfies (cs i) f         -- if it satisfies all the constraints.