non-uniformity in small example

[mflatt]

The formula no_redred-blueblue.txt has 18 solutions. CMSGen generates two of the solutions consistently less often than the others (but we can only because the space of solutions is small enough).

[msoos]

Hi,

Yeah, it seems like you are right, some of the samples are slightly (~20%?) less likely to be output than the rest. In particular,

-1 2 -3 4 -5 6 7 -8 9 -10 -11 12 13 -14 15 -16 -17 18 -19 20 -21 22 -23 -24 -25 26 -27 -28 29 -30 -31 32 -33 -34 35 -36 -37 -38 -39 40 -41 42 -43 44 45 46 -47 48 -49 50 51 52 -53 54 -55 56 57 58 -59 60 -61 62 63 64 -65 66 -67 68 -69 70 71 -72 -73 74 -75 -76 77 -78 -79 80 81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 95 -96 97 98 -99 -100 -101 -102 -103 -104 -105 -106 107 -108 -109 -110 -111 -112 -113 114 115 -116 -117 118 -119 -120 -121 -122 -123 -124 -125 -126 -127 -128 -129 -130 131 132 133 -134 -135 -136 137 -138 139 -140 -141 142 -143 -144 -145 146 -147 -148 -149 -150 151 -152 153 -154 -155 156 -157 -158 -159 160 -161 -162 163 -164 165 -166 167 -168 169 -170 171 -172 173 -174 175 -176 177 -178 179 -180 181 -182 183 0

Seems to be ~20% less likely than the rest. Note that this also happens to be the "smallest" sample, if we order the samples alphabetically.

I took a look around and it's not obvious why this may be. To be honest, it may actually be an issue with the approach. As noted, it's not a guaranteed uniform sampler, only a uniform-like sampler. I think that may just be the case here. Kinda cool that you found such a small & simple problem to demonstrate it with. I think it may allow us to think more about how we could improve the sampler. I have a feeling we could figure out a way to fix it.

What's kinda interesting is that if I preprocess your instance with arjun, our preprocessing tool (available here: https://github.com/meelgroup/arjun), I get this:

p cnf 8 43
c ind 1 2 3 4 5 6 0
-1 -2 -5 -6 0
5 -6 7 -8 0
3 4 5 6 0
1 2 5 6 0
2 4 -5 -7 0
-2 -3 -5 -8 0
1 -2 5 -6 0
-1 4 6 -7 0
-3 -4 -5 -6 0
3 4 7 8 0
3 4 -5 -6 0
5 6 7 8 0
5 6 -7 -8 0
1 -2 3 -4 0
1 -2 7 -8 0
2 -3 -5 8 0
1 2 3 4 0
-1 -2 -3 -4 0
-1 -3 6 8 0
-1 -4 -6 -7 0
-3 4 -7 8 0
1 3 6 8 0
1 2 7 8 0
-1 2 -5 6 0
1 2 -3 -4 0
-1 -2 -7 -8 0
3 -4 7 -8 0
2 3 5 8 0
-5 -6 -7 -8 0
-1 -3 -6 -8 0
3 -4 5 -6 0
1 4 6 7 0
-2 -4 -5 -7 0
-3 -4 -7 -8 0
2 4 5 7 0
1 -4 -6 7 0
1 3 -6 -8 0
-3 4 -5 6 0
-1 2 -3 4 0
-5 6 -7 8 0
-1 2 -7 8 0
-2 -4 5 7 0
-2 3 5 -8 0
c MUST MUTIPLY BY 2**0

This CNF has the same number of solutions -- and they could be relatively easily mapped back to solutions to the original CNF (kinda fun, no? Arjun is powerful). This significantly reduced CNF also exhibits the slanted-sampling behavior under cmsgen -- it consistently has some of the solutions come up less often. This even more simplfied CNF may allow us to understand the problem better. My guess at this point is that cmsgen should: (1) preprocess with arjun (the trivial step), and (2) add variables just at the right places so allow a more even branching heuristic. This second step is really the "trick" but where to add and how is extremely tricky. A form of Bounded Variable Addition is likely what we need, but that's still very little to go on. We'd need to do some statistical analysis to better understand what's happening in order to counter it. Not sure it's worth the effort, but it's an interesting challenge nevertheless.

I hope the above was at least interesting, even if it doesn't help solve the issue (sorry). Note that CMSGen tends to perform significantly better than this on standard, industrial instances. However, so-called "crafted" instances, like the one you have, which essentially tend to encode some kind of game/highly structured hand-written set of rules, seem to be able to break CMSGen. Your example seems to break CMSGen even if I put up the restart cutoff, so that's not the issue. Nice find!

Mate

[yashpote]

The following CNF with 2 variables and 1 clause also leads to biased sampling from cmsgen:

p cnf 2 1
1 2 0
w 1 0.75
w 2 0.75

The sat assignments and their probabilities are:

1 2 -> 0.6
-1 2 -> 0.2
1 -2 -> 0.2

It seems like for any choice of seed and --samples, the fraction of times we see the 1 2 is ~0.56 while it should be 0.6.

I used the commands:
./samplers/cmsgen --samples 1000 --seed 124 test.cnf || grep "^1 2" samples.out | wc -l
561

./samplers/cmsgen --samples 10000 --seed 125 test.cnf || grep "^1 2" samples.out | wc -l
5664

./samplers/cmsgen --samples 100000 --seed 126 test.cnf || grep "^1 2" samples.out | wc -l
56197

[msoos]

Yeah, this is basically known in some sense. CMSGen is not uniform, it's unform-like. It's not that hard to come up with such examples where there is a slight bias. The question is, whether there is a way to fix them in a generic sense. I don't think so, without coming up with a guaranteed uniform sampler. For that, please see https://github.com/meelgroup/unigen