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.
翻译：代表 SAT 实例的图形的视觉布局可以突出 SAT 实例的群落结构。 SAT 实例的群落结构已经与实例硬度和已知条款质量的超常性相关联。 我们的工具 SATViz 以可变互动图和强制导向的布局算法将 CNF 公式视觉化。 有了 SATViz, 条款证明可以被动画, 以不断突出最近学习的条款在移动窗口中出现的变量。 如果需要, SATViz 也可以创建变量互动图的新布局, 与经过调整的边缘重量。 在本文中, 我们描述了 SATViz 的结构和特征组。 我们还展示了与 SATViz 创建的一些有趣的视觉化。
相关内容
微信扫码咨询专知VIP会员