SATViz：子句证明的实时可视化
人工智能
2022-09-14 v1
摘要
表示 SAT 实例的图的可视化布局能够突出 SAT 实例的社区结构。SAT 实例的社区结构既与实例难度相关，也与已知的子句质量启发式相关。我们的工具 SATViz 使用变量交互图和力导向布局算法对 CNF 公式进行可视化。借助 SATViz，子句证明可被动画化，以持续高亮在最近学习子句的移动窗口中出现的变量。如有需要，SATViz 也可利用调整后的边权重新创建变量交互图的布局。在本文中，我们描述 SATViz 的结构与特性集，并展示一些用 SATViz 创建的引人关注的可视化结果。
引用
@article{arxiv.2209.05838,
title = {SATViz: Real-Time Visualization of Clausal Proofs},
author = {Tim Holzenkamp and Kevin Kuryshev and Thomas Oltmann and Lucas Wäldele and Johann Zuber and Tobias Heuer and Markus Iser},
journal= {arXiv preprint arXiv:2209.05838},
year = {2022}
}
备注
Presented at Pragmatics of SAT Workshop (no proceedings)