In 1960, Davis-Putnam procedure was introduced as a theorem-proving technique suitable for automation. It deals with classical propositional and first-order logic. Davis-Putnam procedure deals with a disjunction of clause sets, called a block. This procedure involves repeated rewriting of a block into an equivalent block using simple rewriting rules. Each of these rewriting rules takes some clause set in a block and replace it by one or more of others. The aim is to produce a block that can easily be seen as satisfactory or not.

This could be very successful in practice. Insights from simulated annealing should be very useful. The horizontal axis gives different restart rates. The vertical axis gives the time till solution (logarithmic). We see how one can achieve orders of magnitude speedups by choosing the right restart rate.

Even better restart policies should be achievable by considering a range of  different statistical properties of the search space.

Decision theory group focuses on solving problems with probability and decision theory.  Focus is on making application of these methods practical.  Related methods, approximations, heuristics from AI, OR, Statistics, Economics are applied as needed.  Group’s work typically motivated by real-world problems, e.g., those posed by MS product and systems groups.