Quantified Constraints and Containment Problems

DOI10.2168/LMCS-11(3:9)2015MaRDI QIDQ3196340zbMATH OpenFDO

Authors Hubie Chen, Florent R. Madelaine, Barnaby Martin

Publication date 29 October 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1310.1016

zbMATH Keywords

finite model theoryquantified constraints

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Model theory of finite structures (03C13) Analysis of algorithms and problem complexity (68Q25)

Abstract: The quantified constraint satisfaction problem $mathrmQCSP(mathcalA)$ 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 $mathcalA$. We study two containment problems related to the QCSP. Firstly, we give a combinatorial condition on finite structures $mathcalA$ and $mathcalB$ that is necessary and sufficient to render $mathrmQCSP(mathcalA)subseteqmathrmQCSP(mathcalB)$. We prove that $mathrmQCSP(mathcalA)subseteqmathrmQCSP(mathcalB)$, that is all sentences of positive Horn logic true on $mathcalA$ are true on $mathcalB$, iff there is a surjective homomorphism from $mathcal{A}^{|A{|}^{|B|}}$ to $mathcalB$. This can be seen as improving an old result of Keisler that shows the former equivalent to there being a surjective homomorphism from $mathcal{A}^{o}mega$ to $mathcalB$. We note that this condition is already necessary to guarantee containment of the $P{i}_2$ restriction of the QCSP, that is $P{i}_2$-$mathrmCSP(mathcalA)subseteqP{i}_2$-$mathrmCSP(mathcalB)$. 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 $mathcalA$ together with a fixed $mathcalB$, $|B|=2$, such that there is a surjective homomorphism from $mathcal{A}^r$ to $mathcalB$ only when $rgeq|A|$. Secondly, we prove that the entailment problem for positive Horn fragment of first-order logic is decidable. That is, given two sentences $varphi$ and $psi$ of positive Horn, we give an algorithm that determines whether $varphiightarrowpsi$ 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.

Recommendations

• Computer Science Logic
• The complexity of problems for quantified constraints
• Quantified constraints under perturbation
• Solving quantified constraint satisfaction problems
• Constraints, reduction, and quantization
• Generalizing consistency and other constraint properties to quantified constraints
• Tractable set constraints
• Characterising tractable constraints

Cited in

(4)

• The complexity of problems for quantified constraints
• Quantified Constraints in Twenty Seventeen
• Quantified Equality Constraints
• Decomposing Quantified Conjunctive (or Disjunctive) Formulas

This page was built for publication: Quantified Constraints and Containment Problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3196340)