Stochastic Satisfiability
Artificial intelligence has its roots in logic. The real world often requires us to cope with uncertainty, however, and a numeric framework, rather than the logic-oriented, symbolic one of traditional artificial intelligence, is often useful for expressing such problems. Examples of the numeric approach include Markov decision processes and belief networks. Stochastic satisfiability, a type of logic problem in which some of the variables are associated with probabilities, offers a unique opportunity to combine the strengths of these to approaches in order to develop efficient algorithms for planning and acting under uncertainty.
The courses taught in the Bowdoin Computer Science department are aligned with Assistant Professor Stephen Majercik's Research.
Stochastic Satisfiability Research
Stochastic Boolean satisfiability (SSAT) is a generalization of satisfiability (SAT) that is similar to quantified Boolean satisfiability (QSAT). The ordered variables of the Boolean formula in an SSAT problem, however, instead of being existentially or universally quantified as in a QSAT problem, are existentially or randomly quantified. Randomly quantified variables are True with a certain probability, and an SSAT instance is satisfiable with some probability that depends on the ordering of and interplay between the existential and randomized variables. The goal is to choose values for the existentially quantified variables that maximize the probability of satisfying the formula.
Stephen Majercik has demonstrated the usefulness of stochastic satisfiability (SSAT) by showing that it can provide the foundation for a probabilistic, partially observable, contingent planner that is competitive with other techniques. This approach to planning, implemented in the planner Zander, is based on the fact that this type of planning problem can be converted into an instance of a stochastic satisfiability (SSAT) problem, such that the solution to the SSAT instance yields a plan that will reach the goal with the highest probability.
But, the impact of SSAT research potentially reaches beyond the area of planning under uncertainty. SSAT is a fundamental computer science problem. It is PSPACE-complete and, in the same way that many interesting deterministic problems can be encoded as instances of the NP-complete problem SAT, many probabilistic problems can be encoded as SSAT instances by virtue of the completeness of SSAT. The usefulness of such encodings is just beginning to be explored. In addition to probabilistic planning, SSAT encodings of trust management problems and belief net inferencing problems appear to provide a promising approach to solving these problems. And the study of SSAT may give us new insights into dealing with uncertainty, in general.
Recently, Professor Majercik and Byron Boots (Bowdoin '03) developed a new solver for a particular type of SSAT problem that is several orders of magnitude better than the best known solver in terms of both time and space. Their paper, ''DC-SSAT: A Divide-and-Conquer Approach to Solving Stochastic Satisfiability Problems Efficiently'', was accepted at the prestigious Twentieth National Conference on Artificial Intelligence. They are currently working on extending their results in preparation for a journal version of the paper.
Other research efforts under way in this area include:
1) developing a stochastic local search technique for solving SSAT problems, and
2) investigating the potential benefit of search heuristics tailored to the structure of the particular SSAT problem.