论文标题
使用SAT确定布尔函数的乘法复杂性
Determining the Multiplicative Complexity of Boolean Functions using SAT
论文作者
论文摘要
我们提出了一种基于SAT的建设性算法，以确定布尔函数的乘法复杂性，即，在任何逻辑网络中的最小数量和门由2输入和门组成的逻辑网络中，2输入XOR门和逆变器。为了加快解决时间，我们利用几个对称破坏约束。这些利用XAG的属性可能超出了提出的基于SAT的算法。我们进一步提出了一种启发式优化算法，一旦获得了最佳数量和门，也可以使用SAT求解器，以减少XOR大门的数量。我们的算法能够找到所有5输入仿射等效类的代表以及一组经常出现的6输入功能的所有最佳XAG。
We present a constructive SAT-based algorithm to determine the multiplicative complexity of a Boolean function, i.e., the smallest number of AND gates in any logic network that consists of 2-input AND gates, 2-input XOR gates, and inverters. In order to speed-up solving time, we make use of several symmetry breaking constraints; these exploit properties of XAGs that may be useful beyond the proposed SAT-based algorithm. We further propose a heuristic post-optimization algorithm to reduce the number of XOR gates once the optimum number of AND gates has been obtained, which also makes use of SAT solvers. Our algorithm is capable to find all optimum XAGs for representatives of all 5-input affine-equivalent classes, and for a set of frequently occurring 6-input functions.
