通过采样实现理论的可处理组合
Tractable Combinations of Theories via Sampling
摘要：
对于一阶理论$T$，$T$的约束满足问题是判定给定的原子公式合取在$T$的某个模型中是否可满足的计算问题.在这篇文章中，我们开发的约束满足问题的多项式时间易处理的充分条件的工会的两个理论与不相交的关系签名。为此，我们介绍了抽样理论的概念，并表明抽样可以应用于纳尔逊和奥本的开创性成果不包括的例子。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
