Model Counting: A New Strategy for Obtaining Good Bounds

[gusl]

Carla P. Gomes, Ashish Sabharwal, Bart Selman - Model Counting: A New Strategy for Obtaining Good Bounds tackles the interesting problem of counting the number of assignments satisfying an instance of SAT (the instance is satisfiable if this is >0).

On page 11, they suggest a coin-flipping strategy: each variable assignment flips a coin until there only 1 remaining, and the estimate will be 2^#coin-flips. But they don't explain how one can check that there is only one left. (Also, what if you go from 2 to 0? I imagine that for precision, they probably stop once they get a number < 256... but again, it's not clear how they are counting in the first place)


On page 14, they suggest a way to make assignments flip coins:

Use XOR/parity constraints

...

Which XOR constraint X to use? Choose at random!

Two crucial properties:

* Use XOR/parity constraints
* For every truth assignment A, Pr [ A satisfies X ] = 0.5
* For every two truth assignments A and B, “A satisfies X” and “B satisfies X” are independent

However, what we want is the above probability and independence above to be conditional on A and B being satisfying assignments, otherwise the coin-flips will be biased. I do not see this addressed in the slides.

Comments

[mdinitz.livejournal.com]

My initial thoughts:

I think the point of their paper is that while SAT solvers in practice are really fast, SAT counters are not (which makes sense, since we think that #P is much harder than NP). So for your first question, they're assuming that you just use your favorite SAT solver to check to see if there's at least one solution. And they don't need to check that there's exactly one, just that there's at least one (see page 16 for the algorithm description).

For your second point, I'm not quite sure what you mean. X is not an assignment, it's a parity constraint. They just use it to eliminate assignments randomly. It should be conditional on A and B being satisfying assignments, but that's trivially true since all of the randomness is over the choice of X.

[gustavolacerda.livejournal.com]

Yes, I meant A and B instead of X. Thanks. Fixed.

<< It should be conditional on A and B being satisfying assignments, but that's trivially true since all of the randomness is over the choice of X. >>

I see. The assignment must be found by using a SAT solver. But it still seems *possible* to me for the coin flips to somehow be biased.

* For every two truth assignments A and B, “A satisfies X” and “B satisfies X” are independent.

This seems false to me:
(1) imagine the trivial case where A = B. Done.
(2) Now, suppose A!=B, but they differ only on one variable, x_k. They will disagree whenever X has x_k, and agree otherwise. Maybe conditioning on "A satisfies X" affects the probability of X having x_k? Ok. Anyway, I think this won't generalize to a case where assignments are trinary (0,1,2), but I digress.

I have different non-independence result though:
If we divide the variables V = x_1,...,x_n into two sets: V_left = x1,...,x_k and V_right = x_k+1,...,x_n , and we find that:
* V satisfies A.
* V_left satisfies A.
then it must be the case that V_right satisfies A.

it's linear algebra: imagine the XOR constraints as horizontal vectors (e.g. V = (1 1 ... 1), V_left = (1 ... 1 0 ... 0 ), V_right = (0 ... 0 1 ... 1) ) and the assignments as vertical vectors. The parity of V on assignment A is obtained by multiplying the matrices V A.

Note that V = V_left + V_right.

Therefore V A = V_left A + V_right A.
In particular if V A = 0 and V_left A = 0, then it must be the case that V_right A = 0.

[mdinitz.livejournal.com]

This seems false to me:
(1) imagine the trivial case where A = B. Done.
(2) Now, suppose A!=B, but they differ only on one variable, x_k. They will disagree whenever X has x_k, and agree otherwise. Maybe conditioning on "A satisfies X" affects the probability of X having x_k? Ok. Anyway, I think this won't generalize to a case where assignments are trinary (0,1,2), but I digress.

While it may seem false to you, it's not. You can prove it in general using some basic fourier analysis of boolean functions -- there are lecture notes from both Avrim's learning theory class and Steven Rudich's complexity theory class that do this, if you want to look it up.

As for your other non-independence point, sure, they're only pairwise independent, not three-wise. But that's all that the slide claimed -- you're using three clauses, V, V_left, and V_right instead of A and B (and I'm assuming that in your point when you write A you meant X). In fact, using parity functions is a pretty standard way of taking a small amount of true randomness and generating a large amount of pairwise independent randomness. I haven't looked at their analysis in any detail, but my guess is that they only need pairwise independence.

[gustavolacerda.livejournal.com]

Are you saying that they don't need to qualify their statement to exclude the possibility that A=B?

My (2) was a failed exploration. When I said that it probably wouldn't generalize to trinary, I was giving up refuting the theorem for the binary case (the case that it's really about).

[mdinitz.livejournal.com]

Sure, if A=B then they're not independent. But that's a trivial statement -- I certainly wouldn't include it in conference slides if I was presenting. By the way, if you're interested in this boolean function stuff, and especially in how amazingly cool parity functions are, then Ryan O'Donnell's teaching a class next semester on analysis of boolean functions. It should be fun -- some straight math, some learning theory, and some hardness of approximation stuff.