### 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

• 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, Ξβ)) 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,

• 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 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

• π denotes a set of βvariablesβ
• π· denotes a βdomainβ,
• πΆ denotes an indexed collection of constraints.
``` 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.

```