Constraint Satisfaction Problems (CSPs) are a class of decision problems where one usually fixes a structure A and seeks to decide whether or not a given conjunction of atomic formulas is satisfiable in A or not. It has been shown by Bodirsky and Grohe that every computational decision problem is equivalent to some CSP via a polynomial-time Turing reduction. For structures A with finite domain Zhuk and Bulatov both proved an algebraic criterion classifying in which cases the CSP of A is in P and when it is NP-hard. For some classes of structures with infinite domain, there are similar P vs NP-hard dichotomies.
This thesis continues the latter line of research for CSPs of first-order theories. In this version of CSPs, a theory is fixed and one seeks to decide whether or not a given conjunction of atomic formulas is satisfiable in some model of T. Assuming that the CSPs of theories T1 and T2 are polynomial-time tractable, we prove necessary and sufficient conditions for polynomial-time tractability of the union of T1 and T2. For some classes of theories, P vs NP-hard dichotomies are proven. To achieve this, various 'combinations' of structures are examined, a technique called 'sampling' is generalized to theories and clones of polymorphisms of temporal structures are examined in detail.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:77315 |
| Date | 11 January 2022 |
| Creators | Greiner, Johannes |
| Contributors | Bodirsky, Manuel, Jonsson, Peter, Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, doc-type:doctoralThesis, info:eu-repo/semantics/doctoralThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0018 seconds