Results for the Pseudo-Boolean Evaluation 2015

To check if a result of a solver for a given instance is correct we perform the following checks: We present the results in the tables below, sorting all solvers in alphabetic order. Some remarks: You may note that eight solvers produce some faulty results. This is due to the following reasons: We provide the raw results as a csv file as well. The following data was collected during the evaluation:

To search for a specific instance use the following form:

instance name:

Complete Track


Folderbsolocdcl-cuttingplanesclaspminicardminisatplusnapsopen-wbo open-wbo-lsu pbcplexpblib-pbo2maxsatpblib-pbsolversat4jscipcpxscipspxtoysat
3COL (20)9 15 15 16 16 16 16 0 11 0 15 0 11 10 14
3COL-FromCNF (40)17 30 30 32 32 32 32 0 24 0 30 30 22 22 27
ASP (120)59 (56) 0 98 0 77 91 31 (89) 31 (89) 90 53 76 89 63 63 80
ECGRID-FromCNF (40)23 33 23 23 23 40 40 0 5 0 22 40 11 7 22
EC_ODD_GRIDS (20)12 20 11 11 0 0 20 0 4 0 11 20 18 10 11
EC_RANDOM_GRAPHS (22)7 22 6 7 0 0 6 0 15 0 6 6 21 9 6
EC-RANDOM-GRAPHS-FromCNF (44)13 28 12 14 13 13 14 0 21 0 11 12 25 15 12
minlplib2-pb-0.1.0 (278)14 (1) 0 38 0 27 23 (7) 39 24 62 1 18 17 117 116 25
pbfvmc-formulae (60)12 6 40 0 7 7 0 0 36 0 0 3 34 9 22
ProofComplexity-Extracted-Cardinality-Constraints (1700)724 809 515 623 587 718 737 0 564 0 543 610 588 588 566
SUMINEQ (24)14 24 24 0 0 0 24 0 24 0 24 24 24 24 13
normalized-PB06 (1620)752 (14) 367 805 48 899 944 713 (72) 406 (43) 1043 (10) 251 808 834 1017 (3) 1000 (1) 800
normalized-PB07 (1103)321 70 709 0 384 422 371 (116) 308 (60) 463 550 749 320 835 836 558
normalized-PB09 (268)163 160 212 169 198 209 197 (30) 24 (30) 96 28 194 208 96 96 186
PB10 (6521)4990 3356 5227 1 5107 5321 5138 (255) 1751 (238) 5141 2000 5207 5246 4873 (3) 4605 (3) 5094
PB11 (282)61 (2) 58 87 1 112 104 90 (15) 17 (13) 49 19 74 94 46 47 58
PB12 (2782)39 11 307 8 109 180 (2) 268 (437) 191 (437) 814 (2) 78 80 128 737 (1) 643 (1) 38
ALL (14944)7230 (73) 5009 8159 953 7591 8120 (9) 7736 (1014) 2752 (910) 8462 (12) 2980 7868 7681 8538 (7) 8100 (5) 7532
DEC-LIN-32-CARD (2289)1021 1215 866 953 923 1071 1096 (19) 0 817 0 872 965 850 807 869
OPT-LIN-32-PB (6255)2445 (71) 0 2860 0 2554 2792 (9) 2553 (748) 2453 (774) 3495 (3) 2384 2528 2300 3268 (4) 3078 (4) 2386
OPT-LIN-32-CARD (411)72 0 154 0 207 259 258 (10) 257 (10) 299 162 232 151 292 293 183
OPT-LIN-64-PB (602)0 0 37 0 105 169 65 (143) 42 (126) 0 188 118 189 0 0 60
DEC-LIN-32-PB (4739)3692 (2) 3794 3875 0 3802 3829 3764 (94) 0 3851 (9) 0 3773 3756 3689 (3) 3482 (1) 3756
OPT-NLC-32-PB (350)0 0 240 0 0 0 0 0 0 225 225 239 271 271 171
OPT-NLC-32-CARD (196)0 0 59 0 0 0 0 0 0 21 55 54 93 94 42
OPT-NLC-64-PB (2)0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
DEC-NLC-32-CARD (100)0 0 68 0 0 0 0 0 0 0 65 27 75 75 65

Plots

Below for each category the cactus plots to illustrate the results. Each solver that has at least one faulty result in the category is labeled with "(disqualified)".

DEC-LIN-32-CARD


DEC-LIN-32-PB


DEC-NLC-32-CARD


OPT-LIN-32-CARD


OPT-LIN-32-PB


OPT-LIN-64-PB


OPT-NLC-32-CARD


OPT-NLC-32-PB


Incomplete Track (Fast Track)

We decided to run every solver in the incomplete track (or better called fast track) that is printing the current best model after receiving a SIGTERM signal. After additional 10 secounds we killed the solver process. Hence there are very few results that are marked as faulty due to a timeout during the model printing. But this has no influence on the number of correctly solved instances of the solver.


Folderbsoloclaspminisatplusnapsopen-wbo open-wbo-lsu pbcplexpblib-pbo2maxsatpblib-pbsolversat4jscipcpxscipspxtoysat
3COL (0)0 0 0 0 0 0 0 0 0 0 0 0 0
3COL-FromCNF (0)0 0 0 0 0 0 0 0 0 0 0 0 0
ASP (120)52 (56) 88 39 84 0 31 (89) 83 48 47 76 58 56 71
ECGRID-FromCNF (0)0 0 0 0 0 0 0 0 0 0 0 0 0
EC_ODD_GRIDS (0)0 0 0 0 0 0 0 0 0 0 0 0 0
EC_RANDOM_GRAPHS (0)0 0 0 0 0 0 0 0 0 0 0 0 0
EC-RANDOM-GRAPHS-FromCNF (0)0 0 0 0 0 0 0 0 0 0 0 0 0
minlplib2-pb-0.1.0 (278)11 (1) 33 24 17 (25) 0 23 58 1 16 16 103 106 20
pbfvmc-formulae (30)2 11 4 4 0 0 17 0 0 3 12 5 3
ProofComplexity-Extracted-Cardinality-Constraints (0)0 0 0 0 0 0 0 0 0 0 0 0 0
SUMINEQ (0)0 0 0 0 0 0 0 0 0 0 0 0 0
normalized-PB06 (1201)366 (5) 432 521 564 0 389 (43) 644 (1) 227 432 482 635 622 464
normalized-PB07 (903)221 545 310 342 0 268 (60) 365 543 594 277 656 656 381
normalized-PB09 (99)37 44 24 35 0 25 (30) 36 23 21 37 34 34 23
PB10 (2440)1633 1746 1700 1902 0 1731 (238) 1625 1964 1442 1819 (1) 1304 1246 1698
PB11 (85)14 (1) 19 22 23 0 17 (10) 30 17 16 18 27 27 17
PB12 (2660)16 97 36 69 0 185 (334) 555 (1) 56 41 56 475 412 21
ALL (7816)2352 (63) 3015 2680 3040 (25) 0 2669 (804) 3413 (2) 2879 2609 2784 (1) 3304 3164 2698
Folderbsoloclaspminisatplusnapsopen-wbo open-wbo-lsu pbcplexpblib-pbo2maxsatpblib-pbsolversat4jscipcpxscipspxtoysat
OPT-LIN-32-PB (6255)2283 (63) 2546 2384 2638 (25) 0 2383 (670) 3130 (2) 2297 2041 2174 (1) 2689 2540 2273
OPT-LIN-32-CARD (411)69 148 198 241 0 244 (7) 283 154 217 148 273 276 176
OPT-LIN-64-PB (602)0 33 98 161 0 42 (127) 0 186 80 183 0 0 55
OPT-NLC-32-PB (350)0 230 0 0 0 0 0 225 225 231 263 267 152
OPT-NLC-32-CARD (196)0 58 0 0 0 0 0 17 46 48 79 81 42
OPT-NLC-64-PB (2)0 0 0 0 0 0 0 0 0 0 0 0 0