Random distribution of 2-variable constraints not uniform about pyvsc HOT 5 OPEN

Had some fun with histograms and thought I'd post them here, too. I'll upload my changes once I clean things up. A good excuse for playing around with matplotlib and numpy!

pyvsc (100k samples)

python random.randrange calls (100k samples)
I rewrote the constraints as a conditional and used the random library to get something fast that's similar to what SV outputs to compare with.

from pyvsc.

That looks better! On the histogram it looks like it's a bit more spread out and the hotspots spread out and lowered. Still doesn't have that normal distribution that I think we would want. Although it's been a while since I've thought about probability...

pyvsc triangle (100k samples)

I did want to point out that in a 1M quarter circle constraint in SV the distribution does not appear to be normal. Or at least it tends to have hotspots as well. So I'm not sure what the gold standard for pyvsc should be. Adding multiplication constraints into the mix perhaps makes it harder to guarantee?

from pyvsc.

Hi @alwilson, thanks for putting the work into creating this way to look at 2d distributions. Thus far, I've primarily been looking at 1d distributions -- and that's difficult enough in text format given a reasonably-sized domain.
I'm a bit surprised that the distribution is as skewed as it is, and will need to dig in a bit more to understand why. I find it very interesting that there appear to be hot spots (min a, max b) and (max a, min b) -- hopefully a clue that leads in a productive direction!

Again, thanks for putting together this way to visualize PyVSC distributions. Hopefully I'll shortly have some insights on how to improve the results!

from pyvsc.

The great part about python is all the built in graphing and data crunching tools!

I've seen similar imbalances in my results, but they've been good enough for my uses up to this point.

from pyvsc.

After reviewing the 'swizzling' implementation, I have a better understanding of the hot spots at (min,max) and (max,min). While the variables to swizzle in each solve set are randomly selected, the bits to force in each were being applied sequentially. This increased the probability that few of the bit-force constraints on the second variable would hold, allowing Boolector to repeatedly-select the same solution for the second variable.
Release 0.7.7 randomizes the order in which bit-force constraints are applied. From a visual inspection of text output, this appears to provide a good improvement in multi-variable distribution. Please give the new release a try as you're able.

from pyvsc.