Model Checking Positive Equality-free FO: Boolean Structures and Digraphs of Size Three

TL;DR

This paper classifies the computational complexity of model checking positive equality-free first-order logic over boolean structures and small digraphs, revealing a detailed complexity landscape with dichotomies and tetrachotomies.

Contribution

It provides a complete complexity classification for model checking in these structures, extending understanding of logical decision problems.

Findings

Boolean structures exhibit a dichotomy between Logspace and Pspace-complete.

Digraphs of size ≤3 show a tetrachotomy among Logspace, NP-complete, co-NP-complete, and Pspace-complete.

The results generalize the non-uniform QCSP problem for these classes.

Abstract

We study the model checking problem, for fixed structures A, over positive equality-free first-order logic -- a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(A). We prove a complete complexity classification for this problem when A ranges over 1.) boolean structures and 2.) digraphs of size (less than or equal to) three. The former class displays dichotomy between Logspace and Pspace-complete, while the latter class displays tetrachotomy between Logspace, NP-complete, co-NP-complete and Pspace-complete.