Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Complexity Dichotomy in Spatial Reasoning via Ramsey Theory

Manuel Bodirsky, Bertalan Bodor

Abstract

Constraint satisfaction problems (CSPs) for first-order reducts of finitely bounded homogeneous structures form a large class of computational problems that might exhibit a complexity dichotomy, P versus NP-complete. A powerful method to obtain polynomial-time tractability results for such CSPs is a certain reduction to polynomial-time tractable finite-domain CSPs defined over k-types, for a sufficiently large k. We give sufficient conditions when this method can be applied and illustrate how to use the general results to prove a new complexity dichotomy for first-order expansions of the basic relations of the well-studied spatial reasoning formalism RCC5. We also classify which of these CSPs can be expressed in Datalog. Our method relies on Ramsey theory; we prove that RCC5 has a Ramsey order expansion.

A Complexity Dichotomy in Spatial Reasoning via Ramsey Theory

Abstract

Constraint satisfaction problems (CSPs) for first-order reducts of finitely bounded homogeneous structures form a large class of computational problems that might exhibit a complexity dichotomy, P versus NP-complete. A powerful method to obtain polynomial-time tractability results for such CSPs is a certain reduction to polynomial-time tractable finite-domain CSPs defined over k-types, for a sufficiently large k. We give sufficient conditions when this method can be applied and illustrate how to use the general results to prove a new complexity dichotomy for first-order expansions of the basic relations of the well-studied spatial reasoning formalism RCC5. We also classify which of these CSPs can be expressed in Datalog. Our method relies on Ramsey theory; we prove that RCC5 has a Ramsey order expansion.

Paper Structure

This paper contains 31 sections, 58 theorems, 66 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Countably Categorical Structures
  3. Ramsey Theory
  4. Oligomorphic Clones
  5. Canonical Functions
  6. Behaviours
  7. Canonicity
  8. Canonisation
  9. Complexity
  10. Results
  11. The Unique Interpolation Property
  12. Other Characterisations of the UIP
  13. Proof of the Extension Lemma
  14. Diagonal Interpolation
  15. Rich subsets
  16. ...and 16 more sections

Key Result

Lemma \oldthetheorem

Let $\mathcal{C}$ be a Ramsey class. Then for every $r \in {\mathbb N}$ and $\mathfrak{B} \in \mathcal{C}$ there exists $\mathfrak{C} \in \mathcal{C}$ such that $\mathfrak{C} \to (\mathfrak{B})_r$.

Figures (2)

  • Figure 1: The composition table for the relations of $\mathfrak{R}$.
  • Figure 2: Some structures needed to prove the Ramsey property of $(\mathfrak{R},\prec)$.

Theorems & Definitions (118)

  • Definition 1
  • Lemma \oldthetheorem
  • Theorem \oldthetheorem
  • Proposition \oldthetheorem
  • proof
  • Lemma \oldthetheorem
  • proof
  • proof : Proof of Theorem \ref{['thm:indep']}
  • Definition 2
  • Theorem \oldthetheorem: follows from JBKwonderland
  • ...and 108 more