SATViz: Real-Time Visualization of Clausal Proofs

Visual representations of algorithms can improve our understanding of algorithmic concepts and the nature of the underlying problems. Visualizations of the Conflict-Driven Clause Learning algorithm (CDCL) are of high interest, as this is currently the most successful algorithm for solving the propositional satisfiability problem (SAT problem). Despite the complexity of the SAT problem, implementations of CDCL in so-called SAT solvers are successfully used in industrial practice, e.g., in software verification [4], hardware verification [12], product configuration [21], or planning [18]. For satisfiable instances, SAT solvers output a variable assignment which serves as a certificate of satisfiability. Such a certificate can be checked in polynomial time and hence SAT NP.