Computing differences between tree-structured data is a critical but challenging problem in software analysis. In this paper, we propose a novel tree diffing approach called SatDiff, which reformulates the structural diffing problem into a MaxSAT problem. By encoding the necessary transformations from the source tree to the target tree, SatDiff generates correct, minimal, and type safe low-level edit scripts with formal guarantees. We then synthesize concise high-level edit scripts by effectively merging low-level edits in the appropriate topological order. Our empirical results demonstrate that SatDiff outperforms existing heuristic-based approaches by a significant margin in terms of conciseness while maintaining a reasonable runtime.

翻译：计算树结构数据之间的差异是软件分析中关键但具有挑战性的问题。本文提出一种名为SatDiff的新型树差异比对方法，该方法将结构差异问题转化为MaxSAT问题。通过编码从源树到目标树的必要变换，SatDiff能够生成具有形式化保证的正确、最小且类型安全的底层编辑脚本。随后，我们通过按适当拓扑顺序有效合并底层编辑操作，综合生成简洁的高层编辑脚本。实验结果表明，在保证合理运行时间的前提下，SatDiff在简洁性方面显著优于现有的启发式方法。