Dynamic Programming and Tabled Logic Programming for Encoding Single-Constant Multiplication Into SAT (Declarative Pearls)
摘要
Encoding single-constant multiplication (SCM) constraints into SAT is essential for solving a wide range of combinatorial problems involving integer arithmetic. Although optimal SAT encodings for SCM are known, they are often prohibitively expensive to generate for large constants. This paper introduces a dynamic programming (DP) approach that offers a practical balance between encoding quality and encoding time. The proposed method recursively decomposes the binary representation of the target constant into chunks and eliminates common subexpressions across the chunks and their one’s complements. The objective is either to minimize the number of additions (the min-k objective) or to minimize the number of half/full adders (the min-a objective). The DP algorithm is naturally expressed and efficiently implemented using mode-directed tabling in Picat. Although the approach does not guarantee optimality, experimental results show that it produces high-quality encodings while substantially reducing encoding time. This makes SAT-based techniques considerably more practical for applications involving SCM constraints. The full implementation is publicly available at: https://github.com/nfzhou/Picat/blob/master/scm.pi .