用机器学习加速大数乘法编码，显著降低时间与内存开销。
Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning
- 用图神经网络预测最佳运算符类型，指导分解过程选择
- 在17-32位常数上实现编码时间降1-2个数量级，内存减少97%以上
- 适合硬件设计中需要高效乘法编码的工程师和研究者
单常数乘法（SCM）是硬件设计中的基础NP-hard优化问题，目标是仅用加法、减法和位移操作分解固定常数。尽管动态规划方法可生成近最优的SAT编码，但对大常数而言编码开销仍高。本文提出一种神经符号框架，通过识别引导分解过程运算符选择的良好规则来加速SCM SAT编码。该方法利用图神经网络模型从常数分解中预测有前景的运算符类型，并将置信度分数用于在符号搜索中剪枝无效选择。在未见过的17-32位常数上的实验表明，编码时间降低1至2个数量级，内存使用减少超过97%，分支次数下降一个数量级，同时保持近最优的加法数量。结果表明，学习引导的符号策略能显著提升SCM编码的可扩展性与效率。代码与数据已公开于：https://github.com/Chufeng-Jiang/SCM_MLDP
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。