Disjunctions of Two Dependence Atoms

TL;DR

This paper classifies the computational complexity of model-checking for disjunctions of two dependence atoms, revealing a trichotomy and introducing a new class of 2CNF formulas with LOGSPACE-complete satisfiability.

Contribution

It establishes a comprehensive complexity classification for disjunctions of two dependence atoms, including unary and arbitrary atoms, and characterizes coherence conditions.

Findings

Model-checking for disjunctions of two unary dependence atoms is NL-complete, LOGSPACE-complete, or first-order definable.

The complexity of model-checking for disjunctions of two arbitrary dependence atoms is classified.

A new class of 2CNF formulas with LOGSPACE-complete satisfiability is identified.

Abstract

Dependence logic is a formalism that augments the syntax of first-order logic with dependence atoms asserting that the value of a variable is determined by the values of some other variables, i.e., dependence atoms express functional dependencies in relational databases. On finite structures, dependence logic captures NP, hence there are sentences of dependence logic whose model-checking problem is NP-complete. In fact, it is known that there are disjunctions of three dependence atoms whose model-checking problem is NP-complete. Motivated from considerations in database theory, we study the model-checking problem for disjunctions of two unary dependence atoms and establish a trichotomy theorem, namely, for every such formula, one of the following is true for the model-checking problem: (i) it is NL-complete; (ii) it is LOGSPACE-complete; (iii) it is first-order definable (hence, in AC[0]). Furthermore, we classify the complexity of the model-checking problem for disjunctions of two arbitrary dependence atoms, and also characterize when such a disjunction is coherent, i.e., when it satisfies a certain small-model property. Along the way, we identify a new class of 2CNF-formulas whose satisfiability problem is LOGSPACE-complete.