Multiplication

[vielhuber]

Hello!

This is an awesome project.

I wonder if it is possible to realize integer multiplication of two variable Bits.

At the moment there is only the sum-method available.

Can I somehow execute the sum k-times, where k is another variable (of Logic.variableBits)?

Thanks for your answer.

[danr]

This is a way to roll your own (quadratic multiplication) using the API:

function mul(xs, ys) {
  const bs = []
  const ws = []
  xs.bits.forEach(
    (x, i) =>
      ys.bits.forEach(
        (y, j) => {
          bs.push(Logic.and(x, y))
          ws.push(Math.pow(2, i+j))
        }))
  return Logic.weightedSum(bs, ws)
}

// a little test:
const s = new Logic.Solver()
const x = Logic.variableBits('x', 3)
const y = Logic.variableBits('y', 3)
const xy = Logic.variableBits('xy', 6)
s.require(Logic.equalBits(xy, mul(x, y)))
let sol
while (sol = s.solve()) {
  s.forbid(sol.getFormula())
  console.log({
    x: sol.evaluate(x),
    y: sol.evaluate(y),
    xy: sol.evaluate(xy),
  })
}

[vielhuber]

Cool stuff, thank you. This should deserve a place in README.md.

[vielhuber]

It seems my program is now to heavy on memory.

Currently I get:

MINISAT-out: Cannot enlarge memory arrays. Either (1) compile with -s TOTAL_MEMORY=X with X higher than the current value 67108864, (2) compile with ALLOW_MEMORY_GROWTH which adjusts the size at runtime but prevents some optimizations, or (3) set Module.TOTAL_MEMORY before the program runs.

Is there any way to increase the TOTAL_MEMORY option?

[tranthelam22082003]

I have sample problem MINISAT-out: Cannot enlarge memory arrays. Either (1) compile with -s TOTAL_MEMORY=X with X higher than the current value 67108864, (2) compile with ALLOW_MEMORY_GROWTH which adjusts the size at runtime but prevents some optimizations, or (3) set Module.TOTAL_MEMORY before the program runs.. Is there any way to increase the TOTAL_MEMORY option?