↑ Top


Constraint Satisfaction Problems

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

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

Output

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, Γ’)) is reducible in poly-time to CSP(π’œ)

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

{-# OPTIONS --without-K --exact-split --safe #-}

open import Overture using ( π“ž ; π“₯ ; Signature )

module Base.Complexity.CSP {𝑆 : Signature π“ž π“₯} where

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

-- Imports from the Agda Universal Algebra Library ------------------------------
open import Base.Relations.Continuous       using ( REL ; 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,

module  _              -- levels for...
        {ΞΉ : Level}    -- ...arity (or argument index) types
        {Ξ½ : Level}    -- ...variable symbol types
        {Ξ± β„“ : Level}  -- ... domain types
 where
 open Setoid
 record Constraint (var : Type Ξ½) (dom : var β†’ Setoid Ξ± β„“) : Type (Ξ½ βŠ” Ξ± βŠ” lsuc ΞΉ) where
  field
   arity  : Type ΞΉ               -- The "number" of variables involved in the constraint.
   scope  : arity β†’ var          -- Which variables are involved in the constraint.
   rel    : REL[ i ∈ arity ] (Carrier (dom (scope i)))   -- The constraint relation.

  satisfies : (βˆ€ v β†’ Carrier (dom v)) β†’ 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.

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

 open Algebra
 open Setoid
 record CSPInstance (var : Type Ξ½)(π’œ : var β†’ Algebra Ξ± β„“) : Type (Ξ½ βŠ” Ξ± βŠ” lsuc ΞΉ) where
  field
   ar : Type ΞΉ       -- ar indexes the contraints in the instance
   cs : (i : ar) β†’ Constraint var (Ξ» v β†’ Domain (π’œ v))

  isSolution : (βˆ€ v β†’ Carrier (Domain (π’œ v))) β†’ Type _  -- An assignment *solves* the instance
  isSolution f = βˆ€ i β†’ (Constraint.satisfies (cs i)) f  -- if it satisfies all the constraints.


← Base.Complexity.Basic Top ↑