search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
67 stars 18 forks source link

Fix substitute #30

Closed aljungberg closed 3 years ago

aljungberg commented 3 years ago

Recently the substitute function was fixed to handle an edge case when the object polynomial was a singleton not containing the subject variable (see [#24], [#25]). As far as I can tell that fix is correct for the stated case.

Unfortunately the fix introduced a bug where if the polynomial did contain from_var as a term of its own, all other monomials if any were thrown away.

Example:

  1. in: x(0)*x(7) + x(1) + x(5)
  2. x(1) -> x(5) + x(7)
  3. out: x(5) + x(7) (!)

Informally the buggy substitution method worked like so:

  1. let q = poly / from_var
  2. if q == 1 return to_var

I don't know what definition of this kind of multivariate polynomial division is actually used by BoolePolynomial here, but at a first pass I'd assume A / B, where B is the single variable b, finds quotient Q and remainder R s.t. A = B*Q + R and R has a lower degree in terms of the variable b than A. (Which in GF(2) means degree 0 so there's no b in R.) Then Q == 1 tells us R = A-B, not that A=B!

The code as it was written before #25 had, not withstanding its singleton bug, this implementation for the Q==1 case: poly -= from_var; poly += to_poly;. That might be faster. But it seemed conceptually simpler to me to always calculate and add the remainder.

Ironically I added back an isSingleton test because if quotient is how many b we have in A, and A is a single boolean monomial, and quotient is not 0, then b*quotient is that monomial. So we don't have to go find R (which holds for any degree of Q, not just degree 0).

(This is an area which clearly needs more unit tests and I've contributed one here in the PR.)

This fix also seems to resolve #27!

msoos commented 3 years ago

Wow, thank you so much! Amazing work. I hope you find Bosphorus useful!