论文标题
通过抽样的理论的可处理组合
Tractable Combinations of Theories via Sampling
论文作者
论文摘要
对于一阶理论$ t $，$ t $的约束满意度问题是确定在某些$ t $的某些型号中确定原子公式的给定连词是否可满足的。在本文中，我们开发了足够的条件，以使两种具有不相交关系标志的两种理论的约束满意度问题的多项式障碍性。为此，我们介绍了对理论采样的概念，并表明可以将采样应用于尼尔森和Oppen的开创性结果所涵盖的示例。
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.
