Two-variable logic over two orders has settled finite satisfiability complexity
Two Variables and Two-Dimensional Structures
Logic in Computer Science
Summary
Figuring out if certain logical statements are true when you have two ways to order things was a puzzle for many years. The authors solved three tricky cases about deciding if these statements can be true in finite setups. They found how complex it is to check these statements with two orders and their next-step relations, even with additional helpers. Their findings clarify previous open questions and improve known results, showing that adding extra helpers doesn’t make these problems harder.
What this means in practice
- •For formal methods engineers: Know the exact computational complexity of verifying properties expressed in two-variable logic with two orders to optimize model checking tools.
- •For database query system developers: Use the complexity bounds to guide design of query evaluation engines that involve order constraints and successor relations.
A theory result. No direct application yet.
Authors
Bartosz Jan Bednarczyk, Daumantas Kojelis, Krzysztof Szymański
Abstract
We study the two-variable fragment FO^2 of first-order logic over two-dimensional structures. Formulae may employ two linear orders <=_1, <=_2, their successor relations S_1, S_2, and auxiliary predicates of any arity. Despite two decades of work, three cases of finite satisfiability in this setting were still open; we settle all three. First, finite satisfiability of FO^2 with one linear order and one successor relation, of the same or of a different order, is NExpTime-complete, even with arbitrary auxiliary predicates and constant symbols. This closes a gap left open by Manuel and Zeume (CSL 2013). As an application, a reduction based on swaps of adjacent elements shows that order-invariance and order-successor-invariance of FO^2 are coNExpTime-complete. This reproves the main result of Zeume and Harwath (LICS 2016) and settles their question on order-successor-invariance. Second, finite satisfiability of FO^2 with two linear orders is ExpSpace-hard, already without auxiliary non-unary predicates, matching the upper bound known since 2010. Our reduction combines Kieronski's encoding of alternating Turing machines with the classical fact that the pre-order and post-order traversals of a tree define its descendant relation. Third, with two linear orders and the successor of one of them, finite satisfiability is in ExpSpace even with arbitrary auxiliary predicates, improving the previous 2NExpTime bound and confirming a conjecture of Zeume and Harwath. Together with known results, our theorems show that in two dimensions, auxiliary (non-unary) predicates and constants come for free: with or without them, the complexities coincide. All our proofs are simple.