Activity: Talk or presentation › Contributed talk › unknown
Description
We present DPVIS, a Java tool to visualize the structure of SAT instances
and runs of the DPLL (Davis-Putnam-Logemann-Loveland) procedure.
DPVIS uses advanced graph layout algorithms to display the problems internal
structure arising from its variable dependency (interaction) graph. DPVIS is
also able to generate animations showing the dynamic change of a problems
structure during a typical DPLL run. Besides implementing a simple variant of
the DPLL algorithm on its own, DPVIS also features an interface to MiniSAT, a
state-of-the-art DPLL implementation. Using this interface, runs of MiniSAT can
be visualizedincluding the generated search tree and the effects of clause learning.
DPVIS is supposed to help in teaching the DPLL algorithm and in gaining
new insights in the structure (and hardness) of SAT instances.
Period
20 Jun 2005
Event title
8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT 2005)