Data
Tables
all.html
1.html
cb100.html
Graphs
Cactus plot of all.
Cactus plot were at least one solver needed over 30 seconds.
Cactus plot were at least one solver needed over 50 seconds.
correlation between average SAT time and #SAT calls, 1 vs 100 chunk
correlation between average SAT time and #SAT calls, core based 30 vs 500 chunk
Backbone filtering for 1-chunk
Backbone filtering for core based 100-chunk
Cactus plots for instances split by percentage of backbone literals
0--25.pdf
25--50.pdf
50--75.pdf
75--100.pdf
Where at least one solver took over 50 seconds
0--25_50.pdf
25--50_50.pdf
50--75_50.pdf
75--100_50.pdf
Where at least one solver took over 30 seconds
0--25_30.pdf
25--50_30.pdf
50--75_30.pdf
75--100_30.pdf
Legend
| filename element |
meaning |
| number | size of chunk |
| u | chunk size n |
| cb | corebased |
| l | lifting |
| r | rotating |
| vbs | virtual best solver |