0
addition, subtraction and shiftを使用して2つの数を掛けることは可能です。この手順の重要な部分は、このような操作の最小限の（最適な）シーケンスを見つけることです。ブルートフォースを使用してシーケンスを見つけると、指数関数的に成長するので、さまざまな経験則が使用されます。おそらく最もよく知られているのは、Robert Bernsteinの論文Multiplication by integer constantです。ヴィンセントルフェーブルによってMultiplication by an Integer Constantで与えられるよう、113を掛けるための少数の加算とシフトで定数を掛けること
例：Z3（または類似）を使用することが可能である見つけること：
3x <- x << 1 + x
7x <- 3x << 1 + x
113x <- 7x << 4 + x
私は私は疑問に思ってしまった非常に興味深いanswerつまずい与えられた定数で数を掛ける最小の演算子列？私はこのすべてのSATとSMTにはとても新しいので、ブールの充足可能性の問題の文脈では意味があるのかどうか分かりません。