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.

• Type: Journal
• Year: 2007
• Where: JAR
• Authors: Carsten Sinz
• Keywords: Instance’s Internal Structure, Internal Structure, JAR 2007, Modulo Theories