Sciweavers

JAR
2007

Visualizing SAT Instances and Runs of the DPLL Algorithm

13 years 3 months ago
Visualizing SAT Instances and Runs of the DPLL Algorithm
SAT-solvers have turned into essential tools in many areas of applied logic like, for example, hardware verification or satisfiability checking modulo theories (SMT). And although recent implementations are able to solve problems with hundreds of thousands of variables and millions of clauses, much smaller instances still remain unsolved. What makes a particular instance hard or easy is at most partially understood—and is often attributed to the instance’s internal structure. By converting SAT instances into graphs and applying established graph layout techniques this internal structure can be visualized and thus serve as the basis of subsequent analysis. Moreover, by providing tools that animate the structure during the run of a SAT algorithm, dynamic changes of the problem instance become observable. Thus, we both expect to gain new insights into the hardness of the SAT problem and to help in teaching SAT algorithms.
Carsten Sinz
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where JAR
Authors Carsten Sinz
Comments (0)