meelgroup / approxmc

Approximate Model Counter
Other
70 stars 25 forks source link

Question about probabilistic guarantees over multiple runs #54

Open fanosta opened 6 months ago

fanosta commented 6 months ago

Hi,

I was wondering how the probabilistic guarantees are affected by runnnig ApproxMC on the same model multiple times. I'm thinking that if the seed is the same, we get the same result every time as ApproxMC is designed to be deterministic. But what about multiple runs of the same problem with different seeds? Can these be treated as independent random experiments?

Best, Marcel

msoos commented 6 months ago

I would suggest to simply change epsilon and delta rather than running it multiple times. But yes, both should improve with multiple runs with different seeds. However, @AL-JiongYang has already published code that gives significantly better guarantees for ApproxMC and has been published last year. Once he merges his code change, you should be able to get much better guarantees with the same effort! @AL-JiongYang -- Can you please merge your changes? This is needed by users, as per above.

I hope the above helps! I'll let @AL-JiongYang close this issue once he merged his changes,

Mate

AL-JiongYang commented 6 months ago

Hi Marcel,

Mate's suggestion is correct. It's better to change the epsilon and delta if you only want a stronger guarantee from multiple runs.

To answer your question directly: yes, you are right.

Running ApproxMC on the same problem with different seeds can be treated as independent random experiments. Currently, we use a user-specified random seed to maintain reproducibility, but ideally, we want the seed to be randomly determined by, e.g. the system time, where each run becomes an independent random experiment.

I hope this helps and let me know if you have more questions.

Best, Jiong

fanosta commented 6 months ago

Thank you for the detailed answers 👍

Getting better guarantees for the same effort does sound nice. Especially, if it would also allow me to count larger problems in reasonable time.