Redondo Beach, California
Nov. 12, 2000 to Nov. 14, 2000
G. Gottlob , Tech. Univ. Wien, Austria
P.G. Kolaitis , Tech. Univ. Wien, Austria
T. Schwentick , Tech. Univ. Wien, Austria
Fagin's (1974) theorem, the first important result of descriptive complexity, asserts that a property of graphs is in NP if and only if it is definable by an existential second-order formula. We study the complexity of evaluating existential second-order formulas that belong to prefix classes of existential second-order logic, where a prefix class is the collection of all existential second-order and the first-order quantifiers obey a certain quantifier pattern. We completely characterize the computation complexity of prefix classes of existential second-order logic in three different contexts: over directed graphs; over undirected graphs with self-loops; and over undirected graphs without self-loops. Our main result is that in each of these three contexts a dichotomy holds, i.e., each prefix class of existential second-order logic either contains sentences that can express NP-complete problems or each of its sentences expresses a polynomial-time solvable problem. Although the boundary of the dichotomy coincides for the first two cases, it changes, as one move to undirected graphs without self-loops.
formal logic; computational complexity; graph theory; existential second-order logic; graphs; tractability; descriptive complexity; existential second-order formula; prefix class; first-order quantifiers; computational complexity; directed graphs; undirected graphs; NP-complete problems; polynomial-time solvable problem
G. Gottlob, P.G. Kolaitis, T. Schwentick, "Existential second-order logic over graphs: charting the tractability frontier", FOCS, 2000, 2013 IEEE 54th Annual Symposium on Foundations of Computer Science, 2013 IEEE 54th Annual Symposium on Foundations of Computer Science 2000, pp. 664, doi:10.1109/SFCS.2000.892334