Location: Bowdoin / Computer Science / Student Projects / Oliver Radwan '08

Computer Science

Oliver Radwan '08

Stochastic Boolean Satisfiability (SSAT)

Oliver Radwan '08 and Stephen Majercik As a Surdna Undergraduate Research Fellow during the summer of 2007, Oliver began work with Professor Stephen Majercik to develop a new solution method for Stochastic Boolean Satisfiability (SSAT), a provably difficult problem in Computer Science. He continued this work during the 2007-08 academic year as a successful honors project.

SSAT is one of a number of computer science problems categorized as "PSPACE-complete." Such problems can be solved using a feasible amount of computer memory, but, in general, take an impractical amount of time to solve. SSAT, however, can be used as a framework to model real-world problems, such as probabilistic planning problems, so fast solution techniques for SSAT problems would allow these types of problems to be solved efficiently.

Solutions to SSAT encodings of significant planning problems take the form of large binary "solution trees," and the process of finding the best solution tree involves searching a very large space of trees. For search problems of this type, there are two approaches to searching the solution space: Systematic Search and Local Search.

Figure 6
Figure 6. Satisfaction versus search iterations in multiple BD-SSAT runs on the SSAT encoding of Tiger.2-steps.
Optimal solution percentage of 0.85 is achieved for all runs.

Systematic Search is a type of search that exhaustively examines the entire solution space, methodically checking every possible candidate solution. While this search will eventually find the correct answer, it may take a very long time to examine the entirety of a massive search space. Local Search, on the other hand, quickly finds some candidate solution and then tries to find the best solution by using this as a starting point and repeatedly attempting to improve the current solution. Local Search can sometimes find solutions faster than Systematic Search, but certain characteristics of SSAT problems make it unclear how to apply it to SSAT problems.

Oliver and Professor Majercik worked to combine both types of search in Oliver's honors project, BD-SSAT: Combining Systematic and Local Search to Solve Stochastic Boolean Satisfiability Problems. They developed a solution technique (BD-SSAT) that combines the thoroughness of Systematic Search with the speed of Local Search. BD-SSAT uses Local Search to identify promising areas of the solution space and Systematic Search to explore these areas more thoroughly. This process uses the strengths of each type of search to mitigate the weaknesses of the other. Initial tests showed promising results.