search

master-keying / minisat

A minimalistic and high-performance SAT solver
minisat.se
Other
141 stars 16 forks source link

Improve Minisat::vec<T> implementation and usage #8

Closed horenmar closed 6 years ago

horenmar commented 6 years ago

These two commits first improve the internals of Minisat::vec<T> and then how Minisat itself uses the vector. For more explanations and details see the commit message of the first commit.

Measurements

I did some informal measurements and the performance impact of these changes is either tiny bit beneficial, or imperceivable. On the set of benchmark in the repository, there were no performance regressions.

horenmar commented 6 years ago

For completeness, here are some measurements.

Old timings:

 3/18 Test #240: benchmark:UNSAT/pigeon-hole/hole10.cnf ...   Passed  129.77 sec
 1/18 Test #228: benchmark:SAT/gcp/g250.15.cnf ............   Passed  869.94 sec
 2/18 Test #235: benchmark:SAT/parity/par32-3.cnf .........   Passed  3687.73 sec
 4/18 Test #236: benchmark:SAT/parity/par32-4-c.cnf .......   Passed  3892.80 sec
 5/18 Test #232: benchmark:SAT/parity/par32-2-c.cnf .......   Passed  10934.43 sec
 6/18 Test #234: benchmark:SAT/parity/par32-3-c.cnf .......   Passed  15823.28 sec
 7/18 Test #233: benchmark:SAT/parity/par32-2.cnf .........   Passed  44063.01 sec
 8/18 Test #230: benchmark:SAT/parity/par32-1-c.cnf .......   Passed  44756.81 sec
 9/18 Test #237: benchmark:SAT/parity/par32-4.cnf .........   Passed  51833.27 sec
10/18 Test #238: benchmark:SAT/parity/par32-5-c.cnf .......   Passed  58173.94 sec

With trivial destruction:

 1/18 Test #240: benchmark:UNSAT/pigeon-hole/hole10.cnf ...   Passed  131.98 sec
 2/18 Test #228: benchmark:SAT/gcp/g250.15.cnf ............   Passed  966.06 sec
 3/18 Test #235: benchmark:SAT/parity/par32-3.cnf .........   Passed  3641.41 sec
 4/18 Test #236: benchmark:SAT/parity/par32-4-c.cnf .......   Passed  3837.66 sec
 5/18 Test #232: benchmark:SAT/parity/par32-2-c.cnf .......   Passed  10715.71 sec
 6/18 Test #234: benchmark:SAT/parity/par32-3-c.cnf .......   Passed  15645.41 sec
 7/18 Test #230: benchmark:SAT/parity/par32-1-c.cnf .......   Passed  43980.67 sec
 8/18 Test #233: benchmark:SAT/parity/par32-2.cnf .........   Passed  44131.77 sec
 9/18 Test #237: benchmark:SAT/parity/par32-4.cnf .........   Passed  50946.22 sec
10/18 Test #238: benchmark:SAT/parity/par32-5-c.cnf .......   Passed  58098.01 sec

With pointer-vec, no other changes:

 3/18 Test #240: benchmark:UNSAT/pigeon-hole/hole10.cnf ...   Passed  129.17 sec
 4/18 Test #228: benchmark:SAT/gcp/g250.15.cnf ............   Passed  1014.02 sec
 1/18 Test #235: benchmark:SAT/parity/par32-3.cnf .........   Passed  3661.72 sec
 2/18 Test #236: benchmark:SAT/parity/par32-4-c.cnf .......   Passed  3873.09 sec
 5/18 Test #232: benchmark:SAT/parity/par32-2-c.cnf .......   Passed  11130.70 sec
 6/18 Test #234: benchmark:SAT/parity/par32-3-c.cnf .......   Passed  15903.74 sec
 7/18 Test #233: benchmark:SAT/parity/par32-2.cnf .........   Passed  44191.44 sec
 8/18 Test #230: benchmark:SAT/parity/par32-1-c.cnf .......   Passed  44965.67 sec
 9/18 Test #237: benchmark:SAT/parity/par32-4.cnf .........   Passed  50770.08 sec
10/18 Test #238: benchmark:SAT/parity/par32-5-c.cnf .......   Passed  58300.18 sec

Pointer vec, other changes:

run 1:

 3/18 Test #240: benchmark:UNSAT/pigeon-hole/hole10.cnf ...   Passed  129.17 sec
 4/18 Test #228: benchmark:SAT/gcp/g250.15.cnf ............   Passed  1090.82 sec
 1/18 Test #235: benchmark:SAT/parity/par32-3.cnf .........   Passed  3690.59 sec
 2/18 Test #236: benchmark:SAT/parity/par32-4-c.cnf .......   Passed  3809.05 sec
 5/18 Test #232: benchmark:SAT/parity/par32-2-c.cnf .......   Passed  10651.63 sec
 6/18 Test #234: benchmark:SAT/parity/par32-3-c.cnf .......   Passed  15531.37 sec
 7/18 Test #233: benchmark:SAT/parity/par32-2.cnf .........   Passed  44094.72 sec
 8/18 Test #230: benchmark:SAT/parity/par32-1-c.cnf .......   Passed  44148.59 sec
 9/18 Test #237: benchmark:SAT/parity/par32-4.cnf .........   Passed  50935.27 sec
10/18 Test #238: benchmark:SAT/parity/par32-5-c.cnf .......   Passed  59002.71 sec

run 2:

 3/18 Test #240: benchmark:UNSAT/pigeon-hole/hole10.cnf ...   Passed  127.56 sec
 4/18 Test #228: benchmark:SAT/gcp/g250.15.cnf ............   Passed  939.41 sec
 1/18 Test #235: benchmark:SAT/parity/par32-3.cnf .........   Passed  3671.38 sec
 2/18 Test #236: benchmark:SAT/parity/par32-4-c.cnf .......   Passed  3820.28 sec
 5/18 Test #232: benchmark:SAT/parity/par32-2-c.cnf .......   Passed  10457.01 sec
 6/18 Test #234: benchmark:SAT/parity/par32-3-c.cnf .......   Passed  15693.45 sec
 7/18 Test #233: benchmark:SAT/parity/par32-2.cnf .........   Passed  43865.00 sec
 8/18 Test #230: benchmark:SAT/parity/par32-1-c.cnf .......   Passed  44062.07 sec
 9/18 Test #237: benchmark:SAT/parity/par32-4.cnf .........   Passed  51537.77 sec
10/18 Test #238: benchmark:SAT/parity/par32-5-c.cnf .......   Passed  58592.02 sec

run 3:

 3/18 Test #240: benchmark:UNSAT/pigeon-hole/hole10.cnf ...   Passed  125.96 sec
 4/18 Test #228: benchmark:SAT/gcp/g250.15.cnf ............   Passed  1047.27 sec
 1/18 Test #235: benchmark:SAT/parity/par32-3.cnf .........   Passed  3644.11 sec
 2/18 Test #236: benchmark:SAT/parity/par32-4-c.cnf .......   Passed  3837.87 sec
 5/18 Test #232: benchmark:SAT/parity/par32-2-c.cnf .......   Passed  10617.79 sec
 6/18 Test #234: benchmark:SAT/parity/par32-3-c.cnf .......   Passed  15660.26 sec
 7/18 Test #233: benchmark:SAT/parity/par32-2.cnf .........   Passed  44832.29 sec
 8/18 Test #230: benchmark:SAT/parity/par32-1-c.cnf .......   Passed  45230.90 sec
 9/18 Test #237: benchmark:SAT/parity/par32-4.cnf .........   Passed  51524.86 sec
10/18 Test #238: benchmark:SAT/parity/par32-5-c.cnf .......   Passed  57322.91 sec

Basically the differences between the changes are all around measurement error

The timeouts are always the same:

11/18 Test #239: benchmark:SAT/parity/par32-5.cnf .........***Timeout 86400.01 sec
12/18 Test #226: benchmark:SAT/gcp/g125.17.cnf ............***Timeout 86400.10 sec
13/18 Test #229: benchmark:SAT/gcp/g250.29.cnf ............***Timeout 86400.46 sec
14/18 Test #227: benchmark:SAT/gcp/g125.18.cnf ............***Timeout 86400.56 sec
15/18 Test #225: benchmark:SAT/f/f600.cnf .................***Timeout 86400.57 sec
16/18 Test #231: benchmark:SAT/parity/par32-1.cnf .........***Timeout 86400.57 sec
17/18 Test #223: benchmark:SAT/f/f1000.cnf ................***Timeout 86400.60 sec
18/18 Test #224: benchmark:SAT/f/f2000.cnf ................***Timeout 86400.63 sec
horenmar commented 6 years ago

I cleaned up the PR a bit and after the CI runs, I am going to merge it.

horenmar commented 6 years ago

The AppVeyor failures are spurious (it sometimes fails to clone the repo), so I am going to merge it anyway.