AI 中文总结
研究单常数乘法问题的高效SAT编码，提出神经符号框架，用图神经网络预测运算符类型，利用置信分数修剪搜索选择，实验表明该方法能大幅提升编码的可扩展性与效率，减少时间、内存及分支。
AI 中文摘要
单常数乘法问题是硬件设计中的一个基本NP难优化任务，旨在仅使用加法、减法和移位来分解一个固定常数。虽然动态规划方法可以为单常数乘法生成接近最优的SAT编码，但对于大常数，其编码成本仍然很高。我们提出了一个神经符号框架，通过识别在分解过程中指导运算符选择的良好规则来加速单常数乘法的SAT编码。我们的方法使用图神经网络模型从常数分解中预测有前景的运算符类型，并利用得到的置信分数在符号搜索中修剪不好的选择。对17 - 32位未知常数的实验结果表明，编码时间减少了一到两个数量级，内存使用减少了97%以上，分支减少了一个数量级，同时在加法方面保持了接近最优的编码质量。这些结果表明，学习引导的符号策略可以显著提高单常数乘法编码的可扩展性和效率。我们的代码和数据可在该https URL公开获取。
英文摘要
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
CommentsIn Proceedings ICLP 2026, arXiv:2607.17707
Journal refEPTCS 450, 2026, pp. 81-95
