Computing and Certifying Twin-Width Using Logic

André Schidler

doi:10.1145/3769869

2026-01-01

PRE

André Schidler *

Stefan Szeider

DOI：10.1145/3769869

原文链接

原文求助

摘要

En 中文

孪生宽度是一种强大的图不变量，当输入图的孪生宽度有界时，它支持多种NP难问题的有效求解。一阶模型检测在孪生宽度有界的图类上是固定参数可解的。本研究介绍了两种用于精确计算孪生宽度的算法策略：SAT编码和分支定界方法。SAT编码探索了孪生宽度的不同表述形式，提升了在不同实例类型上的性能；分支定界算法利用缓存的局部解来提高在较大图上的效率。我们提出了一种结合这些方法的验证框架，并获得了可验证的孪生宽度计算证明。我们的研究为孪生宽度计算提供了概念性见解，包括新的收缩顺序和下界及上界技术，这些技术具有独立的研究价值。我们通过严格的实验评估来支持我们的理论发展。

Keyword:

twin-width

sat