Neil Immerman

MFCS Conference 2024 Conference Paper

On the Number of Quantifiers Needed to Define Boolean Functions

• Marco Carmosino
• Ronald Fagin
• Neil Immerman
• Phokion G. Kolaitis
• Jonathan Lenchner
• Rik Sengupta

The number of quantifiers needed to express first-order (FO) properties is captured by two-player combinatorial games called multi-structural games. We analyze these games on binary strings with an ordering relation, using a technique we call parallel play, which significantly reduces the number of quantifiers needed in many cases. Ordered structures such as strings have historically been notoriously difficult to analyze in the context of these and similar games. Nevertheless, in this paper, we provide essentially tight bounds on the number of quantifiers needed to characterize different-sized subsets of strings. The results immediately give bounds on the number of quantifiers necessary to define several different classes of Boolean functions. One of our results is analogous to Lupanov’s upper bounds on circuit size and formula size in propositional logic: we show that every Boolean function on n-bit inputs can be defined by a FO sentence having (1+ε)n/log(n) + O(1) quantifiers, and that this is essentially tight. We reduce this number to (1 + ε)log(n) + O(1) when the Boolean function in question is sparse.

LPAR Conference 2013 Conference Paper

Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning

• Shachar Itzhaky
• Sumit Gulwani
• Neil Immerman
• Shmuel Sagiv

Abstract We describe a framework that combines deductive, numeric, and inductive reasoning to solve geometric problems. Applications include the generation of geometric models and animations, as well as problem solving in the context of intelligent tutoring systems. Our novel methodology uses (i) deductive reasoning to generate a partial program from logical constraints, (ii) numerical methods to evaluate the partial program, thus creating geometric models which are solutions to the original problem, and (iii) inductive synthesis to read off new constraints that are then applied to one more round of deductive reasoning leading to the desired deterministic program. By the combination of methods we were able to solve problems that each of the methods was not able to solve by itself. The number of nondeterministic choices in a partial program provides a measure of how close a problem is to being solved and can thus be used in the educational context for grading and providing hints. We have successfully evaluated our methodology on 18 Scholastic Aptitude Test geometry problems, and 11 ruler/compass-based geometry construction problems. Our tool solved these problems using an average of a few seconds per problem.

AIJ Journal 2012 Journal Article

Applicability conditions for plans with loops: Computability results and algorithms

• Siddharth Srivastava
• Neil Immerman
• Shlomo Zilberstein

The utility of including loops in plans has been long recognized by the planning community. Loops in a plan help increase both its applicability and the compactness of its representation. However, progress in finding such plans has been limited largely due to lack of methods for reasoning about the correctness and safety properties of loops of actions. We present novel algorithms for determining the applicability and progress made by a general class of loops of actions. These methods can be used for directing the search for plans with loops towards greater applicability while guaranteeing termination, as well as in post-processing of computed plans to precisely characterize their applicability. Experimental results demonstrate the efficiency of these algorithms. We also discuss the factors which can make the problem of determining applicability conditions for plans with loops incomputable.

AIJ Journal 2011 Journal Article

A new representation and associated algorithms for generalized planning

• Siddharth Srivastava
• Neil Immerman
• Shlomo Zilberstein

Constructing plans that can handle multiple problem instances is a longstanding open problem in AI. We present a framework for generalized planning that captures the notion of algorithm-like plans and unifies various approaches developed for addressing this problem. Using this framework, and building on the TVLA system for static analysis of programs, we develop a novel approach for computing generalizations of classical plans by identifying sequences of actions that will make measurable progress when placed in a loop. In a wide class of problems that we characterize formally in the paper, these methods allow us to find generalized plans with loops for solving problem instances of unbounded sizes and also to determine the correctness and applicability of the computed generalized plans. We demonstrate the scope and scalability of the proposed approach on a wide range of planning problems.

ICAPS Conference 2011 Conference Paper

Directed Search for Generalized Plans Using Classical Planners

• Siddharth Srivastava 0001
• Neil Immerman
• Shlomo Zilberstein
• Tianjiao Zhang

We consider the problem of finding generalized plans for situations where the number of objects may be unknown and unbounded during planning. The input is a domain specification, a goal condition, and a class of concrete problem instances or initial states to be solved, expressed in an abstract first-order representation. Starting with an empty generalized plan, our overall approach is to incrementally increase the applicability of the plan by identifying a problem instance that it cannot solve, invoking a classical planner to solve that problem, generalizing the obtained solution and merging it back into the generalized plan. The main contributions of this paper are methods for (a) generating and solving small problem instances not yet covered by an existing generalized plan, (b) translating between concrete classical plans and abstract plan representations, and (c) extending partial generalized plans and increasing their applicability. We analyze the theoretical properties of these methods, prove their correctness, and illustrate experimentally their scalability. The resulting hybrid approach shows that solving only a few, small, classical planning problems can be sufficient to produce a generalized plan that applies to infinitely many problems with unknown numbers of objects.

AAAI Conference 2011 Conference Paper

Qualitative Numeric Planning

• Siddharth Srivastava
• Shlomo Zilberstein
• Neil Immerman
• Hector Geffner

We consider a new class of planning problems involving a set of non-negative real variables, and a set of non-deterministic actions that increase or decrease the values of these variables by some arbitrary amount. The formulas specifying the initial state, goal state, or action preconditions can only assert whether certain variables are equal to zero or not. Assuming that the state of the variables is fully observable, we obtain two results. First, the solution to the problem can be expressed as a policy mapping qualitative states into actions, where a qualitative state includes a Boolean variable for each original variable, indicating whether its value is zero or not. Second, testing whether any such policy, that may express nested loops of actions, is a solution to the problem, can be determined in time that is polynomial in the qualitative state space, which is much smaller than the original infinite state space. We also report experimental results using a simple generateand-test planner to illustrate these findings.

AAAI Conference 2011 Conference Paper

Termination and Correctness Analysis of Cyclic Control

• Siddharth Srivastava
• Neil Immerman
• Shlomo Zilberstein

The utility of including cyclic flow of control in plans has been long recognized by the planning community. Loops in a plan increase both its applicability and the compactness of representation. However, progress in finding such plans has been limited largely due to lack of methods for reasoning about the correctness and applicability of loops of actions. We present an overview of recent results for determining the class of problems that a plan with loops can solve. These methods can be used to direct the construction of a rich new form of generalized plans that solve a desired class of problems.

ICAPS Conference 2010 Conference Paper

Computing Applicability Conditions for Plans with Loops

• Siddharth Srivastava 0001
• Neil Immerman
• Shlomo Zilberstein

The utility of including loops in plans has been long recognized by the planning community. Loops in a plan help increase both its applicability and the compactness of representation. However, progress in finding such plans has been limited largely due to lack of methods for reasoning about the correctness and safety properties of loops of actions. We present novel algorithms for determining the applicability and progress made by a general class of loops of actions. These methods can be used for directing the search for plans with loops towards greater applicability while guaranteeing termination, as well as in post-processing of computed plans to precisely characterize their applicability. Experimental results demonstrate the efficiency of these algorithms.

AAMAS Conference 2010 Conference Paper

Merging Example Plans into Generalized Plans for Non-deterministic Environments

• Siddharth Srivastava
• Neil Immerman
• Shlomo Zilberstein

We present a new approach for finding contingent plans with loops andbranches in situations where there is uncertainty instate properties and object quantities, but lack of probabilisticinformation about these uncertainties. We use a state abstractiontechnique from static analysis of programs which uses 3-valued logicto compactly represent belief states with unbounded numbers ofobjects. Our approach for finding plans is to incrementallygeneralize and merge input example plans which can be generated byclassical planners. The expressiveness and scope of this approach aredemonstrated using experimental results on common benchmark domains.

CSL Conference 2007 Conference Paper

Structure Theorem and Strict Alternation Hierarchy for FO 2 on Words

• Philipp Weis
• Neil Immerman

Abstract It is well-known that every first-order property on words is expressible using at most three variables. The subclass of properties expressible with only two variables is also quite interesting and wellstudied. We prove precise structure theorems that characterize the exact expressive power of first-order logic with two variables on words. Our results apply to FO2[<] and FO 2 [<; Suc], the latter of which includes the binary successor relation in addition to the linear ordering on string positions. For both languages, our structuretheorems showexactly whatis expressible using a given quantifier depth, n, and using m blocks of alternating quantifiers, for any m ≤ n. Using these characterizations, we prove, among other results, that there is a strict hierarchy of alternating quantifiers for both languages. The question whether there was such a hierarchy had been completely open. As another consequence of our structural results, we show that satisfiability for FO2[<], which is NEXP-complete in general, becomes NP-complete once we only consider alphabets of a bounded size.

MFCS Conference 2005 Conference Paper

The Complexity of Satisfiability Problems: Refining Schaefer's Theorem

• Eric Allender
• Michael Bauland
• Neil Immerman
• Henning Schnoor
• Heribert Vollmer

Abstract Schaefer proved in 1978 that the Boolean constraint satisfaction problem for a given constraint language is either in P or is NP-complete, and identified all tractable cases. Schaefer’s dichotomy theorem actually shows that there are at most two constraint satisfaction problems, up to polynomial-time isomorphism (and these isomorphism types are distinct if and only if P ≠ NP). We show that if one considers AC 0 isomorphisms, then there are exactly six isomorphism types (assuming that the complexity classes NP, P, ⊕L, NL, and L are all distinct).

CSL Conference 2004 Conference Paper

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics

• Neil Immerman
• Alexander Rabinovich
• Thomas W. Reps
• Shmuel Sagiv
• Greta Yorsh

Abstract To reason effectively about programs, it is important to have some version of a transitive-closure operator so that we can describe such notions as the set of nodes reachable from a program’s variables. On the other hand, with a few notable exceptions, adding transitive closure to even very tame logics makes them undecidable. In this paper, we explore the boundary between decidability and undecidability for transitive-closure logics. Rabin proved that the monadic second-order theory of trees is decidable, although the complexity of the decision procedure is not elementary. If we go beyond trees, however, undecidability comes immediately. We have identified a rather weak language called ∃ ∀ ( DTC + [ E ])that goes beyond trees, includes a version of transitive closure, and is decidable. We show that satisfiability of ∃ ∀ ( DTC + [ E ]) is NEXPTIME complete. We furthermore show that essentially any reasonable extension of ∃ ∀ ( DTC + [ E ]) is undecidable. Our main contribution is to demonstrate these sharp divisions between decidable and undecidable. We also compare the complexity and expressibility of ∃ ∀ ( DTC + [ E ]) with related decidable languages including MSO(trees) and guarded fixed point logics. We mention possible applications to systems some of us are building that use decidable logics to reason about programs.

UAI Conference 2000 Conference Paper

The Complexity of Decentralized Control of Markov Decision Processes

• Daniel S. Bernstein
• Shlomo Zilberstein
• Neil Immerman

Planning for distributed agents with partial state information is considered from a decision- theoretic perspective. We describe generalizations of both the MDP and POMDP models that allow for decentralized control. For even a small number of agents, the finite-horizon problems corresponding to both of our models are complete for nondeterministic exponential time. These complexity results illustrate a fundamental difference between centralized and decentralized control of Markov processes. In contrast to the MDP and POMDP problems, the problems we consider provably do not admit polynomial-time algorithms and most likely require doubly exponential time to solve in the worst case. We have thus provided mathematical evidence corresponding to the intuition that decentralized planning problems cannot easily be reduced to centralized problems and solved exactly using established techniques.

I&C Journal 2000 Journal Article

Tree Canonization and Transitive Closure

• Kousha Etessami
• Neil Immerman

We prove that tree isomorphism is not expressible in the language (FO + TC + COUNT). This is surprising since in the presence of ordering the language captures NL, whereas tree isomorphism and canonization are in L (1992, S. Lindell, in “24th Symp. on Theory of Comput. ” pp. 400–404). Our proof uses an Ehrenfeucht–Fraı̈ssé game for transitive closure logic with counting (1990, E. Grädel, Lecture Notes in Computer Science, Vol. 626, pp. 149–163, Springer-Verlag, Berlin; 1990, N. Immerman and E. Lander, in “Complexity Theory Retrospective, ” pp. 59–81, Springer-Verlag, Berlin). As a corresponding upper bound, we show that tree canonization is expressible in (FO + COUNT)[log n]. The best previous upper bound had been (FO + COUNT)[n O(1)] (1990, P. Dublish and S. Mahesnwari, Lecture Notes in Computer Science, Vol. 452, Springer-Verlag, Berlin). The lower bound remains true for bounded-degree trees, and we show that for bounded-degree trees counting is not needed in the upper bound. These results are the first separations of the unordered versions of the logical languages for NL, AC1, and ThC1. Our results were motivated by our conjecture that (FO + TC + COUNT + 1LO) = NL, i. e. , that a one-way local ordering sufficed to capture NL. We disprove this conjecture, but we prove that a two-way local ordering does suffice, i. e. , (FO + TC + COUNT + 2LO) = NL.

TCS Journal 1996 Journal Article

The expressiveness of a family of finite set languages

• Neil Immerman
• Sushant Patnaik
• David Stemple

In this paper we characterize exactly the complexity of a set-based database language called SRL, which presents a unified framework for queries and updates. By imposing simple syntactic restrictions on it, we are able to express exactly the classes, P and LOGSPACE. We also discuss the role of ordering in database query languages and show that the hom operator of Machiavelli language in [Ohori et al. (1989)] does not capture all the order-independent properties.

TCS Journal 1995 Journal Article

Reachability and the power of local ordering

• Kousha Etessami
• Neil Immerman

The L NL question remains one of the major unresolved problems in complexity theory. Both L and NL have logical characterizations as the sets of totally ordered (⩽) structures expressible in first-order logic augmented with the appropriate Transitive Closure operator (Immerman, 1987): (FO + DTC + ⩽) captures L and (FO + TC + ⩽) captures NL. On the other hand, in the absence of ordering, (FO + TC) is strictly more powerful than (FO + DTC) (Grädel and McColm, 1992). An apparently quite different “structured” model of logspace machines is the Jumping Automaton on Graphs (JAG), (Cook and Rockoff, 1980). We show that the JAG model is intimately related to these logics on “one-way locally ordered” (1LO) structures. We argue that the usual JAG model is unreasonably weak and should be replaced, wherever possible, by the two-way JAG model, which we define. Furthermore, the language (FO + DTC + 2LO) over two-way locally ordered (2LO) graphs is more robust than even the two-way JAG model, and yet lower bounds remain accessible. We prove an upper bound on the power of TC over one-way locally ordered graphs, and three lower bounds on DTC.

FOCS Conference 1989 Conference Paper

An Optimal Lower Bound on the Number of Variables for Graph Identification

• Jin-Yi Cai
• Martin Fürer
• Neil Immerman

It is shown that Omega (n) variables are needed for first-order logic with counting to identify graphs on n vertices. This settles a long-standing open problem. The lower bound remains true over a set of graphs of color class size 4. This contrasts sharply with the fact that three variables suffice to identify all graphs of color class size 3, and two variables suffice to identify almost all graphs. The lower bound is optimal up to multiplication by a constant because n variables obviously suffice to identify graphs on n vertices. >

I&C Journal 1989 Journal Article

Definability with bounded number of bound variables

• Neil Immerman
• Dexter Kozen

A theory satisfies the k-variable property if every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a model of temporal logic satisfies the k-variable property for some k if and only if there exists a finite basis for the temporal connectives over that model. We give a model-theoretic method for establishing the k-variable property, involving a restricted Ehrenfeucht-Fraisse game in which each player has only k pebbles. We use the method to unify and simplify results in the literature for linear orders. We also establish new k-variable properties for various theories of bounded-degree trees, and in each case obtain tight upper and lower bounds on k. This gives the first finite basis theorems for branching-time models of temporal logic.

TCS Journal 1989 Journal Article

Relativizing relativized computations

• Neil Immerman
• Stephen R. Mahaney

This paper introduces a technique of relativizing already relativized computations and gives two interesting applications. The techniques developed here are simpler than the usual methods for constructing oracles that satisfy several requirements simultaneously. The first application shows that a result of Karp and Lipton (if sets in NP are decidable with polynomial-size circuits, then Σ P 2 = Π P 2) cannot be strengthened in the presence of certain oracles. This means that relativizable proof techniques cannot strengthen the conclusion to, say, P=NP. Such a stronger conclusion would be desirable as it would establish the equivalence of polynomial-time programs and polynomial-size circuits for solving NP-complete problems and would extend the known equivalence of polynomial-time programs and programs that are allowed a single query to a polynomial-size table. The second application gives an oracle C for which P C ≠ (NP C ∩ coNP C ) ≠ NP C and NP C ∩ coNP C has complete sets under polynomial-time many-one reductions. This complements a result of Sipser in which an oracle B is constructed for which NP B ∩ coNP B has no complete sets. These results suggest that current proof methods will not settle whether NP ∩ coNP has complete sets.

TARK Conference 1986 Conference Paper

Foundations of Knowledge for Distributed Systems

• Michael J. Fischer
• Neil Immerman

We give a simple, yet very general definition for distributed protocols. We then define notions of knowledgeand common knowledgeappropriate for these protocols. We study how changes in the states of knowledgerelate to more standard notions of computation. We find that by restricting our formulas to certain sets of global states we can realize different, appropriate definitions of knowledge with fundamentally different properties.

STOC Conference 1983 Conference Paper

Languages Which Capture Complexity Classes (Preliminary Report)

• Neil Immerman

STOC Conference 1983 Conference Paper

Sparse Sets in NP-P: EXPTIME versus NEXPTIME

• Juris Hartmanis
• Vivian Sewelson
• Neil Immerman

This paper investigates the structural properties of sets in NP-P and shows that the computational difficulty of lower density sets in NP depends explicitly on the relations between higher deterministic and nondeterministic time-bounded complexity classes. The paper exploits the recently discovered upward separation method, which shows for example that there exist sparse sets in NP-P if and only if EXPTIME @@@@ NEXPTIME. In addition, the paper uses relativization techniques to determine logical possibilities, limitations of these proof techniques, and, for the first time, to exhibit structural differences between relativized NP and CoNP .

STOC Conference 1982 Conference Paper

Relational Queries Computable in Polynomial Time (Extended Abstract)

• Neil Immerman

Query languages for relational databases have received considerable attention. In 1972 Codd [Cod72] showed that two natural mathematical languages for queries—one algebraic and the other a version of first order predicate calculus—had identical powers of expressibility. Query languages which are as expressive as Codd's Relational Calculus are sometimes called complete. This term is misleading, however, because many interesting queries are not expressible in “complete” languages.

FOCS Conference 1980 Conference Paper

Upper and Lower Bounds for First Order Expressibility

• Neil Immerman

We continue the study of first order expressibility as a measure of complexity, introducing the new class Var &Sz[v(n), z(n)] of languages expressible with v(n) variables in sentences of size z(n). We show that when the variables are restricted to boolean values: BVar &Sz[v(n), z(n)] = ASPACE&TIME[v(n), t(n)] That is variables and size correspond precisely to alternating space and time respectively. Returning to variables ranging over an n element universe, it follows that: Var[O(1)] = ASPACE[log n] = PTIME That is the family of properties uniformly expressible with a constant number of variables is just PTIME. These results hold for languages with an ordering on the objects in question, e. g. for graphs a successor relation on the vertices. We introduce an "alternating pebbling game" to prove lower bounds on the number of variables and size needed to express properties without successor. We show, for example, that k variables are needed to express Clique(k), suggesting that this problem requires DTIME[nk].

FOCS Conference 1979 Conference Paper

Length of Predicate Calculus Formulas as a New Complexity Measure

• Neil Immerman

We introduce a new complexity measure, QR[f(n)], which clocks the size of formulas from predicate calculus needed to express a given property. Techniques from logic are used to prove sharp lower bounds in the measure. These results demonstrate space requirements for computations and may provide techniques for seperating Time and Space complexity classes because we show that: NSPACE[f(n)] ⊆ QR[(f(n))2/log(n)] ⊆ DSPACE[f(n)2].

FOCS Conference 1978 Conference Paper

One-Way Log-Tape Reductions

• Juris Hartmanis
• Neil Immerman
• Stephen R. Mahaney

One-way log-tape (1-L) reductions are mappings defined by log-tape Turing machines whose read head on the input can only move to the right. The 1-L reductions provide a more refined tool for studying the feasible complexity classes than the P-time [2, 7] or log-tape [4] reductions. Although the 1-L computations are provably weaker than the feasible classes L, NL, P and NP, the known complete sets for those classes are complete under 1-L reductions. However, using known techniques of counting arguments and recursion theory we show that certain log-tape reductions cannot be 1-L and we construct sets that are complete under log-tape reductions but not under 1-L reductions.