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

[mdinitz]

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]

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

[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

[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).