摘要
单常量乘法（SCM）问题是硬件设计中的一个基本NP难题，旨在仅通过加法、减法和位移来分解一个固定常量。尽管动态规划方法能够生成接近最优的SAT编码，但对于大常量，其编码成本依然较高。我们提出了一种神经符号框架，通过识别良好的规则来加速SCM的SAT编码，从而指导操作符的选择。
我们的方案采用图神经网络模型，从常量分解中预测有前景的操作符类型，并利用生成的置信度分数来剪枝无效选择。在对未见的17-32位常量进行的实验结果显示，编码时间减少了一个到两个数量级，内存使用减少了97%以上，分支数量减少了一个数量级，同时在加法方面保持了接近最优的编码质量。这些结果表明，学习引导的符号策略可以显著提升SCM编码的可扩展性和效率。
我们的代码和数据公开可用，链接：GitHub
博主点评： 该研究通过结合神经网络与符号方法，显著提高了单常量乘法问题的编码效率，展示了机器学习在硬件设计领域的广泛应用潜力，尤其在处理复杂优化任务时，能够有效降低计算资源的消耗。