RESEARCH

I'm interested in systematic methods for solving Boolean satisfiability problems. Stated in a slightly different way; I'm interested in automating propositional proof systems, and I'm particularly interested in proof systems that provide a general and efficient way to describe and reason about problem structure.

Reasoning about problem structure is essential for efficient problem solving. Consider our own human problem solving techniques; human-level cognitive performance rests on our ability to examine vast spaces of possibilities and find good options quickly. We have an innate ability to recognize new problems that are variants of ones previously seen. This type of reasoning is so fundamental to our thinking that we may not even be aware we are doing it.

As a somewhat artificial example, consider the classic ``pigeonhole'' problem: Given n+1 pigeons and n holes, can each pigeon be assigned to its own hole? The answer is obviously no, although the search space is enormous if we enumerate every possible assignment of individual pigeons to specific holes. A human considers only a single such assignment before realizing that all other candidate solutions are essentially the same and need not be investigated separately. Search is unnecessary because all solutions fail for the same reason. This example of human reasoning can be viewed as recognizing and exploiting the problem structure.

I'm currently working with Matt Ginsberg on the ZAP project. We are exploring ways to generalize the exploitation of problem structure across problem domains. At the heart of this effort is a representation and inference system that provides a general and efficient way of both describing and reasoning about problem structure. This system uses a logical representation based on permutation groups. We have implemented an automated version of this proof system that is a Davis-Putnam-Loveland-Logemann (DPLL) style algorithm. The typical underlying procedures such as unit propagation and learning have become group theoretic computations.