Speeding up ApproxMC by reusing models

[yashpote]

Hi,

During the binary search phase, whenever ApproxMC decrements the number of XORs, the models found with a higher number of XORs always satisfy the CNF-XOR with fewer constraints. So we can simply block those and find fewer solutions. For example, for a CNF with 100 variables and 60 x 2^30 solutions, the modified code would look like :-

XORs     SAT calls
1            73
2            73
4            73
8            73
16           73
32           15 (+1 UNSAT) {these 15 models satisfy all instances with fewer XORs}
24           58
28           58
30           45 (+1 UNSAT) {now we have 60 useful models}
29           13            {60 + 13 = 73}

This way, ApproxMC can find, on average, 33% fewer models.

I have modified the code and tested this. There was a speedup of around 25% and 1172/1896 problems were solved, 3 more than the unmodified ApproxMC.

Thanks, Yash

[msoos]

Wow, wanna publish this? Talk with Kuldeep, I think this could be published actually... You are in NUS, right? We'll meet in the summer then, but in the meanwhile, please talk with Kuldeep, I think he would be delighted to hear about these :)

[msoos]

Closing as we should make this a publication and should not discuss this here :)