Tractable Combinations of Theories via Sampling

TL;DR

This paper introduces a new approach using sampling to determine when the combined constraint satisfaction problems of two disjoint theories are solvable in polynomial time, extending previous results.

Contribution

It develops sufficient conditions for polynomial-time solvability of combined theories' CSPs using the novel concept of sampling, surpassing earlier Nelson and Oppen results.

Findings

Sampling can be applied to broader classes of theories.

Sufficient conditions for tractability are established.

Extends the scope of combining theories beyond previous methods.

Abstract

For a first-order theory $T$, the Constraint Satisfaction Problem of $T$ is the computational problem of deciding whether a given conjunction of atomic formulas is satisfiable in some model of $T$. In this article we develop sufficient conditions for polynomial-time tractability of the constraint satisfaction problem for the union of two theories with disjoint relational signatures. To this end, we introduce the concept of sampling for theories and show that samplings can be applied to examples which are not covered by the seminal result of Nelson and Oppen.