Logic, computation and constraint satisfaction

• Main Author: Martin, Barnaby D.
• Published: University of Leicester 2005
• Subjects: 005.1
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.422837

We study a class of non-deterministic program schemes with while loops: firstly, augmented with a priority queue for memory; secondly, augmented with universal quantification; and, thirdly, augmented with universal quantification and a stack for memory. We try to relate these respective classes of program schemes to well-known complexity classes and logics.;We study classes of structure on which path system logic coincides with polynomial time P.;We examine the complexity of generalisations of non-uniform boolean constraint satisfaction problems, where the inputs may have a bounded number of quantifier alternations (as opposed to the purely existential quantification of the CSP). We prove, for all bounded-alternation prefixes that have some universal quantifiers to the outside of some existential quantifiers (i.e. 2 and above), that this generalisation of boolean CSP respects the same dichotomy as that for the non-uniform boolean quantified constraint satisfaction problem.;We study the non-uniform QCSP, especially on digraghs, through a combinatorial analog - the alternating-homomorphism problem - that sits in relation to the QCSP exactly as the homomorphism problem sits with the CSP. We establish a trichotomy theorem for the non-uniform QCSP when the template is restricted to antireflexive, undirected graphs with at most one cycle. Specifically, such templates give rise to QCSPs that are either tractable, NP-complete or Pspace-complete.;We study closure properties on templates that respect QCSP hardness or QCSP equality. Our investigation leads us to examine the properties of first-order logic when deprived of the equality relation.;We study the non-uniform QCSP on tournament templates, deriving sufficient conditions for tractablity, NP-completeness and Pspace-completeness. In particular, we prove that those tournament templates that give rise to tractable CSP also give rise to tractable QCSP.