Search papers, labs, and topics across Lattice.
This paper addresses the Single Constant Multiplication (SCM) problem, a crucial NP-hard optimization challenge in hardware design, by introducing a neuro-symbolic framework that enhances SAT encoding efficiency. By leveraging a graph neural network to predict effective operator types for constant decomposition, the authors achieve substantial reductions in encoding time, memory usage, and branching while maintaining near-optimal encoding quality. Experimental results demonstrate improvements of one to two orders of magnitude in encoding time and over 97% reduction in memory usage for 17-32 bit constants, showcasing the potential of learning-guided strategies in symbolic computation.
Learning-guided strategies can slash SCM SAT encoding time by orders of magnitude while preserving near-optimal quality.
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. Our code and data are publicly available at: https://github.com/Chufeng-Jiang/SCM_MLDP
