This is the Base.Complexity.CSP module of the Agda Universal Algebra Library.
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(π).
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 )
A constraint c consists of
a scope function, s : I β var, and
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.
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.