[Colloq] Eric Robinson Thesis Defense 4/22

[Patricia Freeman]

Eric Robinson will be defending his thesis on Tuesday, 4/22.
The defense will take place in 
Room 366 at 1pm.


Abstract:

The problem of large implicit state space generation is examined.
This has applications in areas such as artificial intelligence, where
it can be used in puzzle search, group theory, where it can be used
in orbit enumeration, and formal verification, where it can be used
in explicit state model checking.  Cases of this problem that
overflow distributed RAM are examined.

Traditionally, two approaches are used for cases that overflow
distributed RAM.  The first approach performs additional computation
in order to allow for the state space to fit in RAM.  The second
approach utilizes disk in a streaming manner in order to use it as an
"extended RAM".  A hybrid approach is presented.  Our technique uses
the available RAM to form an initial approximation of the state
space.  It then goes to disk to discover where this approximation is
incorrect.  We refer to this technique as "Tiered Duplicate
Detection."

With this and other techniques, a hierarchy of implicit state space
generation techniques is built.  We refer to this as the "space-time
search hierarchy."  In it, there is a trade-off between the amount of
computation a technique must perform and the space required by that
technique.  For each technique presented, we offer an analysis of the
run-time and space requirements.  The analysis of the runtime takes
into account the two main components discussed here, the number of
computations along with the amount of data accessed on disk.

Finally, we offer an API and corresponding software for the problem of
large implicit state space generation.  Using this API, we implement
our technique, Tiered Duplicate Detection, along with some sample
applications.  With this, we demonstrate three things:  that the
implementation of applications in our API is straightforward and
fast; that our software can be used to effectively solve problems in
large implicit state space generation; and that our analysis of the
runtimes for these techniques are accurate when compared to the
experimental times seen.