用常数乘最少的加和移

Question

只使用加法、减法和移位就可以将两个数字相乘。该过程的重要部分是找到这类操作的最小(最优)序列。使用蛮力寻找序列会导致难度的指数增长，因此使用了各种启发式方法，也许最常见的是Robert的论文整数常数乘法。

例如，如文森特·莱费夫尔( Vincent )在整数常数乘法中给出的那样，乘数为113：

  3x <-  x << 1 + x
  7x <- 3x << 1 + x
113x <- 7x << 4 + x

我偶然发现了一个非常有趣的回答，这让我想知道:是否可以使用Z3 (或类似的)来找到最小的运算符序列来乘以给定的常量？我对SAT和SMT非常陌生，所以我不确定它在布尔可满足性问题的上下文中是否有意义？

Answer 1

这确实是可能的。但是请注意，这个问题是NP-困难的。

不久前，我们做了一个关于一个更普遍的问题(多重常数乘法)的实验：http://web.ist.utl.pt/nuno.lopes/pubs/mcm-pb10.pdf

基本上，结果非常令人失望。专门的算法要快得多。