利用布尔可满足性方法寻找最优的常数矩阵乘法电路

《IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems》：Discovering Optimal Constant Matrix Multiplication Circuits With Boolean Satisfiability

本文提出一种基于布尔可满足性问题的方法，用于优化常数矩阵乘法（CMM）电路设计，将乘法转换为加/减/移位操作，并证明其最优性。该方法可应用于数字滤波器、卷积核心和FFT等场景，显著降低硬件复杂度。

　　

摘要：

在设计算术电路时，可以通过一系列加法/减法和移位操作来实现变量与常数的乘法，而无需使用乘法运算（例如：7x=23x?x=(x?3)?x)。这种方法可以显著降低乘法电路的复杂性，因为加法器的硬件效率通常比通用乘法器更高，并且通过适当连接相关信号，移位操作可以毫无开销地完成。这一概念扩展到了常数矩阵与变量向量的乘法，即常数矩阵乘法（Constant Matrix Multiplication，简称CMM）。目前，还没有一种方法能够找到加法/减法次数最少的CMM算法。在这里，我们展示了如何将CMM问题转化为一系列布尔可满足性（Boolean Satisfiability，简称SAT）问题，从而可以利用强大的SAT求解器来确定任意矩阵的最优解。在封闭的数学框架中对问题进行建模，使我们能够直接将算法扩展到其他目标，例如减少加法/减法操作的字长以及通过流水线技术来最大化吞吐量。与现有的启发式方法相比，即使对于较小的实际矩阵尺寸（如2×2或3×3），我们也始终能够提高实现复杂性。这些成果有助于降低各种实际应用的实现成本，例如数字滤波器、人工神经网络中的卷积核心，或者在离散变换（如快速傅里叶变换）中对复数的乘法运算。

引言

在数字滤波器实现[1]、[2]、[3]、快速傅里叶变换（FFT）[4]或人工神经网络推理[5]等实际应用中，变量与常数的乘法是一个常见的操作。在这项工作中，我们提出了第一种用于常数矩阵与向量乘法的无乘法器电路的最优方法。对于给定的常数矩阵，该方法通过反复构建和解决布尔可满足性（SAT）问题来确定电路，并证明不存在更优的电路（从电路复杂性的角度来看）。