Body Text

Second Level

Third Level

Fourth Level

Fifth Level

Page ‹#›

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.