2026/07/20 by Chufeng Jiang, Neng-Fa Zhou, Neng‐Fa Zhou
Computer Science · Engineering · #Numerical Methods and Algorithms #Low-power high-performance VLSI design #Cryptography and Residue Arithmetic
paper · pdf · doi:10.4204/eptcs.450.6
The Single Constant Multiplication problem is a fundamental NP-hard optimization task in hardware design, which seeks to decompose a fixed constant using only additions, subtractions, and bit-shifts.Although dynamic programming methods can produce near-optimal SAT encodings for SCM, their encoding cost remains high for large constants.We propose a neuro-symbolic framework that accelerates SCM SAT encoding by identifying good rules for guiding operator selection during decomposition.Our approach employs a graph neural network model to predict promising operator types from constant decompositions, and exploits the resulting confidence scores to prune no-good choices in the symbolic search.Experimental results on unseen 17-32 bit constants demonstrate one to two orders of magnitude reductions in encoding time, over 97% reduction in memory usage, and an order-of-magnitude decrease in branching, while preserving near-optimal encoding quality in terms of additions.These results show that learning-guided symbolic strategies can significantly improve the scalability and efficiency of SCM encoding.