Communications - June 2011

Doi: 10.1145/1953122.1953149

Technical Perspective
The Quest for a Logic for
Polynomial-Time Computation
By Phokion G. Kolaitis

the iNteractioN BetWeeN computation and logic goes back to the early beginnings of computer science with the development of computability theory in the 1930s by A. Turing, K. Gödel, A. Church, S. Kleene, and the other great logicians of that era. In more recent decades, the interaction between computation and logic has spanned the entire spectrum of computer science, from programming languages to artificial intelligence and from computational complexity to database systems. Consider, for example, the P vs. NP problem, which is justly regarded to be the central open problem in theoretical computer science. 1 Formally, the P vs. NP problem asks whether or not the class NP of all algorithmic problems solvable by a non-deterministic Turing machine in polynomial time coincides with the class P of all algorithmic problems solvable by a deterministic Turing machine in polynomial time. Informally, the P vs. NP problem asks whether every algorithmic problem whose solutions can be efficiently verified has the property that its solutions can also be efficiently computed. Logic has played a key role in the investigation of this problem. Indeed, in 1971, S. Cook established the existence of “hardest” problems in NP by showing that Boolean Satisfiability, a fundamental problem in propositional logic, is NP-complete. This implies that P = NP if and only if there is an efficient algorithm for telling whether or not a given Boolean formula has a satisfying truth assignment.

Soon after Cook’s seminal discovery, R. Fagin found an even tighter connection between logic and NP by showing that NP coincides with the class of all algorithmic problems that can be specified using a logical formalism known as existential second-order logic or, in short, ESO. To illustrate this result, consider

3-Colorability, another prominent NP- complete problem, which asks whether or not a given graph G (that is, a set of nodes V and a set of edges E) can be colored by assigning one of three colors, say blue, red, and yellow, to each of its nodes, so that no two nodes joined by an edge have the same color. This problem can be specified by the ESO -formula shown at the bottom of the page.

Intuitively, this formula asserts that the set V of nodes can be partitioned into three subsets (color classes) B, R, and Y such that if two nodes x and y are joined by an edge E(x, y), then x and y cannot be in the same color class. Fagin’s result reinforces the unity between computation and logic by providing a logic-based, machine-free characterization of NP that makes no mention of computational resources (time) or bounds ( polynomial) on such resources.

Is there a logic for P In other words, is there a logical formalism L on the class of all graphs such P coincides with the class of all algorithmic problems on graphs that can be specified in L? This problem was raised by Y. Gurevich in 1984, who actually conjectured that there is no logic for P. A related (and essentially equivalent) problem had been raised in 1982 by A. Chandra and D. Harel, who asked: is there is an algorithm that enumerates all polynomial-time computable properties of graphs? Having a logic L for P will make it possible to recast the P vs. NP problem as a problem of pure logic, namely, as the problem of whether or not ESO and L have the same expressive power on the collection of all graphs. Furthermore, a logic L for P will serve as a high-level specification language for expressing precisely those algorithmic problems about graphs whose solutions can be efficiently computed.

The quest for a logic for P on the
class of all graphs has been going on for
the past 30 years. While the problem
remains unresolved to date, the quest
has given rise to a fascinating journey
that has brought together several dif-
ferent strands of research. The follow-
ing paper by Martin Grohe contains an
account of one of the most sophisti-
cated and beautiful results obtained to
date in the quest for a logic for P on the
class of all graphs. In a nutshell, Grohe
shows there is indeed a logic for P for
many large classes of graphs of algo-
rithmic interest and mathematical sig-
nificance. More precisely, his result as-
serts that there is a logic for P for every
class of graphs consisting of all graphs
that exclude some fixed graph as a mi-
nor, that is, as a graph obtained by edge
contractions on a subgraph. This result
vastly generalizes earlier work showing
that a logic for P exists for large classes
of graphs, including the class of all pla-
nar graphs.

References

1. Fortnow, l. the status of the P versus nP problem.

Commun. ACM 52, 9 (sept. 2009), 78–86.

Phokion G. Kolaitis ( kolaitis@cs.ucsc.edu) is a professor of computer science at the university of California santa Cruz and a research staff member at IbM research— almaden.