---
layout: default
title : "Legacy.Base.Complexity.CSP module (The Agda Universal Algebra Library)"
date : "2021-07-14"
author: "the agda-algebras development team"
---

### <a id="constraint-satisfaction-problems">Constraint Satisfaction Problems</a>

> **Deprecated**.  Canonical home is now [`Setoid.Complexity.CSP`](/Setoid/Complexity/CSP/), ported under #307 (M2-7c).  Importers will see `WARNING_ON_USAGE` warnings on `Constraint` and `CSPInstance`; migrate by replacing `Legacy.Base.Complexity.CSP` with `Setoid.Complexity.CSP` (signature parameter is unchanged).  See [`src/Legacy/Base/DEPRECATED.md`](../../DEPRECATED.md).  Removal is planned for v3.1.

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

#### <a id="the-relational-formulation-of-csp">The relational formulation of CSP</a>

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(π’œ).

#### <a id="connection-to-algebraic-csp">Connection to algebraic CSP</a>

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).


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

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

module Legacy.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 Legacy.Base.Relations.Continuous       using ( REL ; REL-syntax )
open import Setoid.Algebras.Basic  {𝑆 = 𝑆}  using ( Algebra )
```


#### <a id="constraints">Constraints</a>

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"


```agda
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.
```

#### <a id="csp-templates-and-instances">CSP templates and instances</a>

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.

```agda
 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.
```

```agda
{-# WARNING_ON_USAGE Constraint   "Use Setoid.Complexity.CSP.Constraint instead. Deprecated under #307; removal planned one minor cycle later." #-}
{-# WARNING_ON_USAGE CSPInstance  "Use Setoid.Complexity.CSP.CSPInstance instead. Deprecated under #307; removal planned one minor cycle later." #-}
```