A Contraction Tree SAT Encoding for Computing Twin-Width
摘要
Twin-width is a structural width parameter and matrix invariant introduced by Bonnet et al. [FOCS 2020], that has been gaining attention due to its various fields of applications. In this paper, inspired by the SAT approach of Schidler and Szeider [ALENEX 2022], we provide a new SAT encoding for computing twin-width. The encoding aims to encode the contraction sequence as a binary tree. The asymptotic size of the formula under our encoding is smaller than in the state-of-the-art relative encoding of Schidler and Szeider. We also conduct an experimental study, comparing the performance of the new encoding and the relative encoding.