0

It is possible to multiply two numbers by using just addition, subtraction and shift. The important part of the procedure is to find the minimal (optimal) sequence of such operations. Using brute force to find the sequence leads to exponential growth of difficulty so various heuristics are used, perhaps the most commonly known is the paper Multiplication by integer constant by Robert Bernstein.

Example for multiplying by 113, as given in Multiplication by an Integer Constant by Vincent Lefevre:

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

I stumbled upon a very interesting answer which got me wondering: would it be possible to use Z3 (or similar) to find the minimal sequence of operators to multiply numbers by the given constant? I'm very new to all this SAT and SMT so I'm not sure if it makes sense at all in the context of Boolean satisfiability problem?

Community
  • 1
  • 1
Ecir Hana
  • 10,864
  • 13
  • 67
  • 117

1 Answers1

0

It is indeed possible. Note however that the problem is NP-hard.

We did an experiment a while ago with a more general problem (multiple constant multiplication): http://web.ist.utl.pt/nuno.lopes/pubs/mcm-pb10.pdf

Basically the results were pretty disappointing. Specialized algorithms were much faster.

Nuno Lopes
  • 868
  • 6
  • 13
  • AFAIK, it is just conjectured to be NP-hard. I have read 2 old articles claiming to prove the NP-completeness of some variant of SCM or MCM, but they were both wrong (one because the reformulation of the problem was plainly incorrect, and IIRC, the other one was wrong for NP-hard and regarded NP as obvious, which isn't if one doesn't artificially bound the shift count). – vinc17 Nov 08 '18 at 12:46