Base.Complexity.CSP module (The Agda Universal Algebra Library)

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

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,

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.

← Base.Complexity.Basic Top ↑