Eric Wallace, Nicholas Tomlin, Albert Xu, Kevin Yang, Eshaan Pathak, Matthew Ginsberg, Dan Klein. Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). 2022.

We introduce a new notion of systematicity for satisfiability algorithms with restarts, saying that an algorithm is strongly systematic if it is systematic independent of restart policy but weakly systematic if it is systematic for some restart policies but not others. We show that existing satisfiability engines are generally only weakly systematic, and describe FLEX, a strongly systematic algorithm that uses an amount of memory polynomial in the size of the problem. On large number factoring problems, FLEX appears to outperform weakly systematic approaches.

The Green Driver app is a dynamic routing application for GPS-enabled smartphones. Green Driver combines client GPS data with real-time traffic light information provided by cities to determine optimal routes in response to driver route requests. Routes are optimized with respect to travel time, with the intention of saving the driver both time and fuel, and rerouting can occur if warranted. During a routing session, client phones communicate with a centralized server that both collects GPS data and processes route requests. All relevant data are anonymized and saved to databases for analysis; statistics are calculated from the aggregate data and fed back to the routing engine to improve future routing. Analyses can also be performed to discern driver trends: where do drivers tend to go, how long do they stay, when and where does traffic congestion occur, and so on. The system uses a number of techniques from the field of artificial intelligence. We apply a variant of A* search for solving the stochastic shortest path problem in order to find optimal driving routes through a network of roads given light-status information. We also use dynamic programming and hidden Markov models to determine the progress of a driver through a network of roads from GPS data and light-status data. The Green Driver system is currently deployed for testing in Eugene, Oregon, and is scheduled for large-scale deployment in Portland, Oregon, in Spring 2011.

This is the third of three papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high-performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal has been to define a representation in which this structure is apparent and can be exploited to improve computational performance. The first paper surveyed existing work that (knowingly or not) exploited problem structure to improve the performance of satisfiability engines, and the second paper showed that this structure could be understood in terms of groups of permutations acting on individual clauses in any particular Boolean theory. We conclude the series by discussing the techniques needed to implement our ideas, and by reporting on their performance on a variety of problem instances.

This is the second of three planned papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal is to define a representation in which this structure is apparent and can easily be exploited to improve computational performance. This paper presents the theoretical basis for the ideas underlying ZAP, arguing that existing ideas in this area exploit a single, recurring structure in that multiple database axioms can be obtained by operating on a single axiom using a subgroup of the group of permutations on the literals in the problem. We argue that the group structure precisely captures the general structure at which earlier approaches hinted, and give numerous examples of its use. We go on to extend the Davis-Putnam-Logemann-Loveland inference procedure to this broader setting, and show that earlier computational improvements are either subsumed or left intact by the new method. The third paper in this series discusses ZAP's implementation and presents experimental performance results.

This is the first of three planned papers describing ZAP, a satisfiability engine that substantially generalizes existing tools while retaining the performance characteristics of modern high-performance solvers. The fundamental idea underlying ZAP is that many problems passed to such engines contain rich internal structure that is obscured by the Boolean representation used; our goal is to define a representation in which this structure is apparent and can easily be exploited to improve computational performance. This paper is a survey of the work underlying ZAP, and discusses previous attempts to improve the performance of the Davis-Putnam-Logemann-Loveland algorithm by exploiting the structure of the problem being solved. We examine existing ideas including extensions of the Boolean language to allow cardinality constraints, pseudo-Boolean representations, symmetry, and a limited form of quantification. While this paper is intended as a survey, our research results are contained in the two subsequent articles, with the theoretical structure of ZAP described in the second paper in this series, and ZAP's implementation described in the third.

This paper investigates the problems arising in the construction of a program to play the game of contract bridge. These problems include both the difficulty of solving the game's perfect information variant, and techniques needed to address the fact that bridge is not, in fact, a perfect information game. GIB, the program being described, involves five separate technical advances: partition search, the practical application of Monte Carlo techniques to realistic problems, a focus on achievable sets to solve problems inherent in the Monte Carlo approach, an extension of alpha-beta pruning from total orders to arbitrary distributive lattices, and the use of squeaky wheel optimization to find approximately optimal solutions to cardplay problems. GIB is currently believed to be of approximately expert caliber, and is currently the strongest computer bridge program in the world.

This paper extends existing work on the use of default information to describe planning hierarchies in two ways. First, we present a completeness result showing that all hierarchical planners can be described using defaults. Second, we show that if t

Because of their occasional need to return to shallow points in a search tree, existing backtracking methods can sometimes erase meaningful progress toward solving a search problem. In this paper, we present a method by which backtrack points can be moved deeper in the search space, thereby avoiding this difficulty. The technique developed is a variant of dependency-directed backtracking that uses only polynomial space while still providing useful control information and retaining the completeness guarantees provided by earlier approaches.

The paper by Sacks and Doyle that is the focus of this debate resembles previous papers by Cheeseman and McDermott, leaping from the observation that a specific application of some AI technology is unable to solve a problem to the conclusion that the technology itself is of limited value. We argue that claims such as this should be made more cautiously in the future, and make constructive suggestions about future qualitative physics research based on Sacks and Doyle's results.

A bilattice is a set equipped with two partial orders and a negation operation that inverts one of them while leaving the other unchanged; it has been suggested that the truth values used by inference systems should be chosen from such a structure instead of the two-point set {t, f}. Given such a choice, we redefine a modal operator to be a function on the bilattice selected. We show that this definition generalizes both Kripke's possible worlds approach and Moore's autoepistemic logic, and also use recent developments in the formalization of logic programs to construct a procedure for determining the truth value of a sentence when the underlying knowledge base involves modal operators of this form.

We present a computationally effective approach to representing and reasoning about actions with many qualifications. The approach involves treating actions as qualified not by specific facts that may or may not hold when the action is executed, but instead as potentially qualified by general constraints describing the domain being investigated. Specifically, we suggest that the result of the action be computed without considering these qualifying domain constraints, and take the action to be qualified if and only if any of the constraints is violated after the computation is complete. Our approach is presented using the framework developed in [6], where we discussed a solution to the frame and ramification problems based on the notion of possible worlds, and compared the computational requirements of that solution to the needs of more conventional ones. In the present paper, we show that the domain constraint approach to qualification, coupled with the possible worlds approach described earlier, has the remarkable property that essentially no computational resources are required to confirm that an action is unqualified. As before, we also make a quantitative comparison between the resources needed by our approach and those required by other formulations.

This paper describes a uniform formalization of much of the current work in artificial intelligence on inference systems. We show that many of these systems, including first‐order theorem provers, assumption‐based truth maintenance systems (atmss), and unimplemented formal systems such as default logic or circumscription, can be subsumed under a single general framework. We begin by defining this framework, which is based on a mathematical structure known as abilattice.We present a formal definition of inference using this structure and show that this definition generalizes work involving atmss and some simple nonmonotonic logics. Following the theoretical description, we describe a constructive approach to inference in this setting; the resulting generalization of both conventional inference and atmss is achieved without incurring any substantial computational overhead. We show that our approach can also be used to implement a default reasoner, and discuss a combination of default and atms methods that enables us to formally describe an “incremental” default reasoning system. This incremental system does not need to perform consistency checks before drawing tentative conclusions, but can instead adjust its beliefs when a default premise or conclusion is overturned in the face of convincing contradictory evidence. The system is therefore much more computationally viable than earlier approaches. Finally, we discuss the implementation of our ideas. We begin by considering general issues that need to be addressed when implementing a multivalued approach such as that we are proposing, and then turn to specific examples showing the results of an existing implementation. This single implementation is used to solve a digital simulation task using first‐order logic, a diagnostic task using atmss as suggested by de Kleer and Williams, a problem in default reasoning as in Reiter's default logic or McCarthy's circumscription, and to solve the same problem more efficiently by combining default methods with justification information. All of these applications use the same general‐purpose bilattice theorem prover and differ only in the choice of bilattice being considered.

Counterfactuals are a form of common-sense nonmonotonic inference that has been of long-term interest to philosophers. In this paper, we begin by describing some of the impact counterfactuals can be expected to have in artificial intelligence, and by reviewing briefly some of the philosophical conclusions which have been drawn about them. We continue by presenting a formal description of counterfactual implication and discussing the issues involved in implementing it. Specific applications in the domains of planning and the automated diagnosis of hardware faults are considered, and we conclude by describing possible extensions to this work involving multi-valued logics and situation semantics.