We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
QUANTIFIED CONSTRAINTS AND CONTAINMENT PROBLEMS.
- Authors
HUBIE CHEN; MADELAINE, FLORENT; MARTIN, BARNABY
- Abstract
The quantified constraint satisfaction problem QCSP(A) is the problem to decide whether a positive Horn sentence, involving nothing more than the two quantifiers and conjunction, is true on some fixed structure A. We study two containment problems related to the QCSP. Firstly, we give a combinatorial condition on finite structures A and B that is necessary and sufficient to render QCSP(A) ⊆ QCSP(B). We prove that QCSP(A) ⊆ QCSP(B), that is all sentences of positive Horn logic true on A are true on B, iff there is a surjective homomorphism from A∣A∣∣B∣ to B. This can be seen as improving an old result of Keisler that shows the former equivalent to there being a surjective homomorphism from Aω to B. We note that this condition is already necessary to guarantee containment of the Π2 restriction of the QCSP, that is Π2-CSP(A) ⊆ Π2-CSP(B). The exponent's bound of ∣A∣∣B∣ places the decision procedure for the model containment problem in non-deterministic double-exponential time complexity. We further show the exponent's bound ∣A∣∣B∣ to be close to tight by giving a sequence of structures A together with a fixed B, ∣B∣ = 2, such that there is a surjective homomorphism from Ar to B only when r ≥∣A∣. Secondly, we prove that the entailment problem for positive Horn fragment of first-order logic is decidable. That is, given two sentences Φ and ψ of positive Horn, we give an algorithm that determines whether Φ → ψ is true in all structures (models). Our result is in some sense tight, since we show that the entailment problem for positive first-order logic (i.e. positive Horn plus disjunction) is undecidable. In the final part of the paper we ponder a notion of Q-core that is some canonical representative among the class of templates that engender the same QCSP. Although the Q-core is not as well-behaved as its better known cousin the core, we demonstrate that it is still a useful notion in the realm of QCSP complexity classifications.
- Subjects
HOMOMORPHISMS; MATHEMATICAL functions; MORPHISMS (Mathematics); COMPUTABILITY logic; MATHEMATICAL analysis
- Publication
Logical Methods in Computer Science (LMCS), 2015, Vol 11, Issue 3, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.2168/LMCS-11(3:9)2015