论文标题
Satviz：clausal证明的实时可视化
SATViz: Real-Time Visualization of Clausal Proofs
论文作者
论文摘要
代表SAT实例的图表的视觉布局可以突出显示SAT实例的社区结构。 SAT实例的社区结构与实例硬度和已知条款质量启发式方法有关。 Our tool SATViz visualizes CNF formulas using the variable interaction graph and a force-directed layout algorithm.借助SATVIZ，可以对条款证明进行动画，以连续突出在最近学习子句的移动窗口中发生的变量。如果需要，Satviz还可以使用调整后的边缘权重创建可变交互图的新布局。在本文中，我们描述了Satviz的结构和特征集。我们还提出了一些使用Satviz创建的有趣的可视化。
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.
