Efficient Tree Diffing Using SAT Solving: A Formal Approach to Generating Minimal and Type-Safe Edit Scripts

The authors propose a novel tree diffing approach called SatDiff, which reformulates the structural diffing problem into a MaxSAT problem. SatDiff generates correct, minimal, and type-safe low-level edit scripts with formal guarantees, and then synthesizes concise high-level edit scripts by effectively merging low-level edits in the appropriate topological order.