meelgroup / approxmc

Approximate Model Counter
Other
70 stars 26 forks source link

fix the bug about reusing models #19

Closed AL-JiongYang closed 3 years ago

AL-JiongYang commented 3 years ago

In terms of reusing models, we want to reuse all the models from larger hashes and reuse models from smaller hashes as much as possible by checking if models from smaller hashes satisfy xors in the current hash.

As for reusing models from smaller hashes, I can understand the condition here aims to speed up because the model from a too-small hash probably won't satisfy xors now. However, such a condition may cause a repeat of models. For example, we find a model M1 when using 16 xors. Then, increase to 32 xors and won't reuse any model because 32-16>9. Therefore, it's possible that we find the same model M1 when using 32 xors. Next, we jump back to 24 (in the middle of 16 and 32) xors and possibly reuse the M1 from 16 xors (because 24-16<9) and M1 from 32 xors at the same time because we don't check if the model is repeated. As a result, the model M1 is counted twice, which finally results in a wrong answer.

Therefore, we can either remove the condition to reuse all the possible models, or check the repeat of models, in order to fix the bug.

The probability of the corner case above is quite small and the deviation imposed on the final answer is slight, so we may not recognize the bug in most cases.

msoos commented 3 years ago

Thanks so much for catching this!!

That optimization is probably premature, to be honest. The slowdown is probably almost non-existent. We should check, but it should be near 0% time. Merging!