Model Counting: A New Strategy for Obtaining Good Bounds
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.
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.