SATViz: Real-Time Visualization of Clausal Proofs

TL;DR

SATViz is a tool for real-time visualization of SAT instance graphs and clause proofs, aiding understanding of instance structure and proof dynamics through interactive visualizations.

Contribution

This paper introduces SATViz, a novel visualization tool that animates clause proofs and allows dynamic graph layout adjustments for SAT instances.

Findings

Enhanced visualization of clause proofs.

Insight into community structure and hardness.

Flexible graph layout capabilities.

Abstract

Visual layouts of graphs representing SAT instances can highlight the community structure of SAT instances. The community structure of SAT instances has been associated with both instance hardness and known clause quality heuristics. Our tool SATViz visualizes CNF formulas using the variable interaction graph and a force-directed layout algorithm. With SATViz, clause proofs can be animated to continuously highlight variables that occur in a moving window of recently learned clauses. If needed, SATViz can also create new layouts of the variable interaction graph with the adjusted edge weights. In this paper, we describe the structure and feature set of SATViz. We also present some interesting visualizations created with SATViz.