Model Counting: A New Strategy for Obtaining Good Bounds

[gustavolacerda]

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

Comments

[gustavolacerda]

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]

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]

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]

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.