Es ist möglich, zwei Zahlen zu multiplizieren, indem Sie nur addition, subtraction and shift verwenden. Der wichtige Teil des Verfahrens besteht darin, die minimale (optimale) Abfolge solcher Operationen zu finden. Brute Force zu verwenden, um die Sequenz zu finden, führt zu exponentiellem Wachstum der Schwierigkeit, so dass verschiedene Heuristiken verwendet werden, vielleicht am bekanntesten ist das Papier Multiplication by integer constant von Robert Bernstein.Multiplikation mit Konstante in den wenigsten Hinzufügungen und Verschiebungen
Beispiel mit 113 zu multiplizieren, wie in Multiplication by an Integer Constant von Vincent Lefevre gegeben:
3x <- x << 1 + x
7x <- 3x << 1 + x
113x <- 7x << 4 + x
ich auf ein sehr interessanten answer gestolpert, die mich fragen, bekamen: wäre es möglich, Z3 zu verwenden (oder ähnlich) zu finden die minimale Folge von Operatoren, um Zahlen mit der gegebenen Konstante zu multiplizieren? Ich bin sehr neu in all dem SAT und SMT, also bin ich mir nicht sicher, ob es überhaupt Sinn macht im Zusammenhang mit dem booleschen Erfüllbarkeitsproblem?