Overview Download References/Contact
DPvis is 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 problem’s internal structure arising from its variable dependency (interaction) graph. DPvis is also able to generate animations showing the dynamic change of a problem’s 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 visualized—including 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.

Functionality:

  • Visualization of a SAT instance's interaction graph, revealing the problem's internal structure
  • Visualization of the search tree generated by a basic DPLL algorithm
  • Visualization of runs generated by MiniSAT, a state-of-the-art DPLL algorithm that also implements advanced features like clause learning or search restarts.

Main Features:

  • Two different graph layout algorithms (force-directed layouts) to show the problem-inherent structure (symmetries, variable dependencies, clusters, ...)
  • Zooming into the interaction graph and panning to focus on areas of special interest
  • Setting of variables' values to true/false with automatic subsequent unit propagation
  • Free navigation in the DPLL search tree
  • Possibility to re-compute the layout of the interaction graph at each node of the search tree.

DPvis is a valuable tool for:

  • Building hypotheses on why a given SAT instance is hard or easy for a DPLL SAT solver
  • Teaching the basic DPLL algorithm and recent extensions of it, like clause learning and restarts. By having an integrated view on both the problem structure (via its variable interaction graph) and the search tree, students can obtain a good intuition how the DPLL method works.

Have fun working with DPvis!