The Complexity of Positive First-Order Logic without Equality II: The Four-Element Case

We study the complexity of evaluating positive equality-free sentences of first-order (FO) logic over fixed, finite structures B. This may be seen as a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(B). Extending the algebraic methods of a previous paper, we derive a complete complexity classification for these problems as B ranges over structures of domain size 4. Specifically, each problem is either in L, is NP-complete, is co-NP-complete or is Pspace-complete.

• Type: Conference
• Year: 2010
• Where: CSL
• Authors: Barnaby Martin, Jos Martin
• Keywords: Automated Reasoning, CSL 2010, Finite Structures B, Non-uniform Quantified Constraint, Positive Equality-free Sentences