Dissertation Defense Details

Algorithm Capability and Applications in Artificial Intelligence

Abstract

Many algorithms are known to work well in practice on a variety of different problem instances. Reusing existing algorithms for problems besides the one that they were designed to solve is often quite valuable. This is accomplished by transforming an instance of the new problem into an input for the algorithm and transforming the output of the algorithm into the correct answer for the new problem. To capitalize on the efficiency of the algorithm, it is essential that these transformations are efficient. Clearly not all problems will have efficient transformations to a particular algorithm so there are limitations on the scope of an algorithm.

An example of this concept will be presented in proving the exact capability of DPLL which is the most well known algorithm for solving Satisfiability (SAT). It has been well studied and is continuously being optimized in an effort to develop faster SAT solvers. The amount of work being done on optimizing DPLL makes it a good candidate for solving other problems. The notion of algorithm capability proved useful in applying DPLL to two areas of AI: Planning and Nonmonotonic Reasoning. Planning is PSPACE Complete in general, but NP Complete when restricted to problems that have polynomial length plans. Trying to optimize the plan length or introducing preferences increases the complexity of the problem. Despite the fact that these problems are harder than SAT, they are with in the scope of what DPLL can handle. Most problems in nonmonotonic reasoning are also harder than SAT. Despite this fact, DPLL is a candidate solution for nonmonotonic logics. The complexity of nonmonotonic reasoning in general is beyond the scope of what DPLL can handle. By knowing the capability of DPLL, one can analyze subsets of nonmonotonic reasoning that it can be used to solve. For example, DPLL is capable of solving the problem of model checking in normal default logic. Again, this problem is harder than SAT, but can still be solved with a single call to a SAT solver. The idea of algorithm capability led to the fascinating discovery that SAT solvers can solve problems that are harder than SAT.