Performance of WinSat

To test the performance of WinSat we generated 6 random problems using WinSat, and applied different algorithms to these problems. The comparison was done against ubcsat which is a great program for empirical analysis. A great deal of algorithms have been implemented in ubcsat. Here, we tested all these algorithms using their default settings, and we reported the best performing algorithms on the problems instance we generated. In addition, we applied a combination of gsat, K-Means and walksat (which is gwsat in ubcsat) to the random problems, and reported the results in the following table.

A few points about the results:

  • Unsat in the table below is not necessarily the best possible cost. We could have run the different algorithms longer or fine tuned the different parameters to obtain better results, however,  it is our intention to show the gain obtained by applying K-Means.
  • The combination of gsat/K-Means/walksat yield great results in comparison to all other algorithms.
  • The implementation of WinSat's walksat (ubcsat's gwsat) is extermely fast (the same goes for gsat).
  • Although WinSat's walksat doesn't improve the results much after an order of magnitude more flips than ubcsat's gwsat it doesn't mean that WinSat's walksat is any less efficient (or in anyway different an algorithm). One should appreciate the amount of work that needs to be done by a search algorithm to satisfy those remaining unsatisfied clauses.
  • Given the previous point, the gain obtained by K-Means is not superficial. The few clauses that become satisfied by the combination can't be easily obtained via walksat or gsat alone.

You can perform the same tests yourself to see how well the algorithms perform. The parameters that were set for the combination, gsat/K-Means/walksat were as follows:

  • Initial assignments: 200
  • gsat run 1,000,000 flips on each assignment
  • K-Means centroids: 5
  • walksat run 40,000,000 flips on each of the 5 centroids.

 

n

ratio

Algorithm

Total number of flips

Time

Unsat
20,000 6 WinSat GSAT/K-Means/WALKSAT 2x108 (GSAT) + 2x108 (WALKSAT) 17.8 min 1539
20,000 6 UBCSAT GWSAT 108 51.0 min 1602
20,000 6 WinSat WALKSAT 109 1.08 hours 1593
20,000 6 UBCSAT IROTS 3x107 52.3 min 1631
20,000 8 WinSat GSAT/K-Means/WALKSAT 2x108 (GSAT) + 2x108 (WALKSAT) 24.1 min 3916
20,000 8 UBCSAT GWSAT 108 51.9 min 3953
20,000 8 WinSat WALKSAT 109 1.56 hours 3944
20,000 8 UBCSAT IROTS 3x107 50.8 min 4049
20,000 10 WinSat GSAT/K-Means/WALKSAT 2x108 (GSAT) + 2x108 (WALKSAT) 31.2 min 6621
20,000 10 UBCSAT GWSAT 108 52.1 min 6722
20,000 10 WinSat WALKSAT 109 1.94 hours 6693
20,000 10 UBCSAT IROTS 3x107 50.34 min 6699
50,000 6 WinSat GSAT/K-Means/WALKSAT 2x108 (GSAT) + 2x108 (WALKSAT) 30 min 8684
50,000 6 UBCSAT GWSAT 108 1.98 hours 8853
50,000 6 WinSat WALKSAT 109 1.82 hours 8789
50,000 6 UBCSAT IROTS 3x107 2.15 hours 8821
50,000 8 WinSat GSAT/K-Means/WALKSAT 2x108 (GSAT) + 2x108 (WALKSAT) 36 min 15955
50,000 8 UBCSAT GWSAT 108 2.04 hours 19194
50,000 8 WinSat WALKSAT 109 2.2 hours 15992
50,000 8 UBCSAT IROTS 3x107 1.96 hours 16321
50,000 10 WinSat GSAT/K-Means/WALKSAT 2x108 (GSAT) + 2x108 (WALKSAT) 47 min 23838
50,000 10 UBCSAT GWSAT 108 2.11 hours 24206
50,000 10 WinSat WALKSAT 109 2.83 hours 24075
50,000 10 UBCSAT IROTS 3x107 2.23 hours 24384

 

If you have any problems with WinSAT or would like to report a bug, please send me an email at:

Dr. Mohamed Qasem mqasem@gmail.com

Back to the home page