Name
Abstract | ||
|---|---|---|
The CSP of a first-order theory T is the problem of deciding for a given finite set S of atomic formulas whether T boolean OR S is satisfiable. Let T-1 and T-2 be two theories with countably infinite models and disjoint signatures. Nelson and Oppen presented conditions that imply decidability (or polynomial-time decidability) of CSP(T1 boolean OR T2) under the assumption that CSP(T-1) and CSP(T-2) are decidable (or polynomial-time decidable). We show that for a large class of omega-categorical theories T1; T2 the Nelson-Oppen conditions are not only sufficient, but also necessary for polynomial-time tractability of CSP(T1 boolean OR T2) (unless P=NP). |
Year | DOI | Venue |
|---|---|---|
2020 | 10.23638/LMCS-16(1:21)2020 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | DocType | Volume |
Complexity,Combination,Constraint Satisfaction Problem,CSP,First-order Theory,countably categorical,homogeneous,Nelson-Oppen | Journal | 16 |
Issue | ISSN | Citations |
1 | 1860-5974 | 0 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Manuel Bodirsky | 1 | 644 | 54.63 |
| Johannes Greiner | 2 | 0 | 0.68 |