DPvis -- a tool to visualize the structure of SAT instances 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 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.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Shishmarev, Maxim; Mears, Christopher; Tack, Guido; Garcia de la Banda, Maria: Visual search tree profiling (2016)
- Newsham, Zack; Lindsay, William; Ganesh, Vijay; Liang, Jia Hui; Fischmeister, Sebastian; Czarnecki, Krzysztof: $\mathsf SATGraf$: visualizing the evolution of SAT formula structure in solvers (2015)
- Orbe, Ezequiel; Areces, Carlos; Infante-López, Gabriel: iSAT: structure visualization for SAT problems (2012)
- Audemard, Gilles; Jabbour, Said; Sais, Lakhdar: SAT graph-based representation: A new perspective (2008)
- Sinz, Carsten: Visualizing SAT instances and runs of the DPLL algorithm (2007)
- Biere, Armin; Sinz, Carsten: Decomposing SAT problems into connected components (2006)
- Sinz, Carsten; Dieringer, Edda-Maria: DPvis -- a tool to visualize the structure of SAT instances (2005)