Problems of computationally reasoning how an agent should act under a given set of circumstances have in the past been framed deterministically; the agent knows with certainty the state of its environment and the consequences of its actions. These assumptions of certainty severely constrain the applicability of techniques developed to solve such problems because the assumptions ignore the uncertainties inherent in most real-world systems. In part to address the shortcomings of this deterministic planning paradigm, Professor Majercik and his colleagues have pioneered the study of stochastic satisfiability, or SSAT. In general, SSAT extends the classic computer science problem satisfiability, or SAT, by incorporating uncertainty. The SSAT problem is PSPACE-complete and, therefore, important theoretically, but SSAT also has practical applications. An instance of a broad class of planning problems in which the agent is unsure of the state of its environment and/or the results of its actions can be efficiently transformed into an SSAT problem such that the solution to the SSAT problem is the solution to the planning problem. Because the SSAT problem is PSPACE-complete, it is likely that the same technique can be applied to other important, practical problems. In order for this technique to be successfully applied, however, one must be able to solve the resulting SSAT problem efficiently.
In his work over the summer, Mark investigated how the properties of SSAT problems and the use of different SSAT solution algorithms influence the time and space required to solve random SSAT problem instances. Mark implemented an SSAT solution technique based on the classic Davis-Putnam-Logemann-Loveland algorithm for solving SAT problems and used this solution technique within a framework that allowed him to track and statistically analyze the resources used by the algorithm over the course of solving many random problems. By changing either the parameterization of the random problems or by modifying the solution algorithm, he hoped to understand which factors influenced the solution process and in what ways. He found in particular that certain properties of the underlying SSAT instances are very important in determining empirical solution difficulty, while others have only small effects. Understanding how these factors influence the solution difficulty will be critical for designing new SSAT solution techniques and techniques for representing planning problems as SSAT instances.
Mark plans to continue his work in computer science in general and on SSAT in particular during the 2006-2007 academic year. He intends to further explore the SSAT problem by investigating non-random problem instances and by creating more intuitive, graphical tools for algorithmic analysis of SSAT solvers. The insights and tools emerging from such work will help introduce other computer science students to the fascinating subject of stochastic satisfiability.
Summer Research at Bowdoin: Artificial Intelligence Researcher Revels in the Impossible