Label | Meaning |
---|---|
S | Solution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A} |
O | Best solution found |
T | CPU time (TO for Time Out) |
(out)(err) | Standard output and standard error for each solver |
Color | Meaning for Complete Solvers | Meaning for Incomplete Solvers |
---|---|---|
Text | Best solver column | Best solver column |
Text | Optimal solution with the best CPU time | Best solution with the best CPU time |
Text | Optimal solution and finished within the Time Out | Best solution without the best CPU time |
Text | Optimal solution and did not finish within the Time Out | Solution found but not the best |
Text | Time Out | Time Out |
Text | Buggy solution | Buggy solution |
Instance file name | Best solver | Sat4j-i | ubcsat-irots |
---|---|---|---|
frb10-6-1.wcnf | O = 50 T = 1.98 |
O = 50 T = 2.74 (out)(err) |
O = 50 T = 1.98 (out)(err) |
frb10-6-2.wcnf | O = 50 T = 1.88 |
O = 50 T = 3.61 (out)(err) |
O = 50 T = 1.88 (out)(err) |
frb10-6-3.wcnf | O = 50 T = 2.00 |
O = 50 T = 3.70 (out)(err) |
O = 50 T = 2.00 (out)(err) |
frb10-6-4.wcnf | O = 50 T = 2.63 |
O = 50 T = 2.63 (out)(err) |
O = 50 T = 2.67 (out)(err) |
frb15-9-1.wcnf | O = 120 T = 5.06 |
O = 122 T = 8.92 (out)(err) |
O = 120 T = 5.06 (out)(err) |
frb15-9-2.wcnf | O = 120 T = 4.91 |
O = 122 T = 135.60 (out)(err) |
O = 120 T = 4.91 (out)(err) |
frb15-9-3.wcnf | O = 120 T = 4.58 |
O = 122 T = 47.56 (out)(err) |
O = 120 T = 4.58 (out)(err) |
frb15-9-4.wcnf | O = 120 T = 5.23 |
O = 122 T = 12.19 (out)(err) |
O = 120 T = 5.23 (out)(err) |
frb15-9-5.wcnf | O = 120 T = 1.20 |
O = 121 T = 213.64 (out)(err) |
O = 120 T = 1.20 (out)(err) |
frb20-11-1.wcnf | O = 200 T = 13.93 |
O = 204 T = 55.93 (out)(err) |
O = 200 T = 13.93 (out)(err) |
frb20-11-2.wcnf | O = 200 T = 8.00 |
O = 204 T = 28.86 (out)(err) |
O = 200 T = 8.00 (out)(err) |
frb20-11-3.wcnf | O = 200 T = 16.72 |
O = 204 T = 103.65 (out)(err) |
O = 200 T = 16.72 (out)(err) |
frb20-11-4.wcnf | O = 200 T = 11.35 |
O = 205 T = 3.48 (out)(err) |
O = 200 T = 11.35 (out)(err) |
frb20-11-5.wcnf | O = 200 T = 95.93 |
O = 204 T = 2.30 (out)(err) |
O = 200 T = 95.93 (out)(err) |
frb25-13-1.wcnf | O = 301 T = 28.68 |
O = 305 T = 83.33 (out)(err) |
O = 301 T = 28.68 (out)(err) |
frb25-13-2.wcnf | O = 301 T = 29.52 |
O = 306 T = 2.52 (out)(err) |
O = 301 T = 29.52 (out)(err) |
frb25-13-3.wcnf | O = 301 T = 62.01 |
O = 307 T = 3.91 (out)(err) |
O = 301 T = 62.01 (out)(err) |
frb25-13-4.wcnf | O = 301 T = 47.03 |
O = 305 T = 38.97 (out)(err) |
O = 301 T = 47.03 (out)(err) |
frb25-13-5.wcnf | O = 302 T = 13.46 |
O = 306 T = 3.85 (out)(err) |
O = 302 T = 13.46 (out)(err) |
frb30-15-1.wcnf | O = 423 T = 37.80 |
O = 427 T = 3.04 (out)(err) |
O = 423 T = 37.80 (out)(err) |
frb30-15-2.wcnf | O = 423 T = 19.80 |
O = 428 T = 4.76 (out)(err) |
O = 423 T = 19.80 (out)(err) |
frb30-15-3.wcnf | O = 422 T = 60.02 |
O = 428 T = 4.54 (out)(err) |
O = 422 T = 60.02 (out)(err) |
frb30-15-4.wcnf | O = 423 T = 21.33 |
O = 430 T = 5.04 (out)(err) |
O = 423 T = 21.33 (out)(err) |
frb30-15-5.wcnf | O = 423 T = 20.46 |
O = 429 T = 3.26 (out)(err) |
O = 423 T = 20.46 (out)(err) |
frb35-17-1.wcnf | O = 565 T = 27.99 |
O = 570 T = 4.12 (out)(err) |
O = 565 T = 27.99 (out)(err) |
frb35-17-2.wcnf | O = 564 T = 207.56 |
O = 568 T = 5.32 (out)(err) |
O = 564 T = 207.56 (out)(err) |
frb35-17-3.wcnf | O = 564 T = 28.38 |
O = 572 T = 2.20 (out)(err) |
O = 564 T = 28.38 (out)(err) |
frb35-17-4.wcnf | O = 564 T = 12.75 |
O = 572 T = 4.33 (out)(err) |
O = 564 T = 12.75 (out)(err) |
frb35-17-5.wcnf | O = 564 T = 41.87 |
O = 571 T = 5.75 (out)(err) |
O = 564 T = 41.87 (out)(err) |
frb40-19-1.wcnf | O = 726 T = 35.98 |
O = 731 T = 4.43 (out)(err) |
O = 726 T = 35.98 (out)(err) |
frb40-19-2.wcnf | O = 725 T = 38.62 |
O = 731 T = 5.10 (out)(err) |
O = 725 T = 38.62 (out)(err) |
frb40-19-3.wcnf | O = 727 T = 35.85 |
O = 729 T = 7.47 (out)(err) |
O = 727 T = 35.85 (out)(err) |
frb40-19-4.wcnf | O = 726 T = 231.62 |
O = 731 T = 4.65 (out)(err) |
O = 726 T = 231.62 (out)(err) |
frb40-19-5.wcnf | O = 726 T = 132.59 |
O = 732 T = 15.65 (out)(err) |
O = 726 T = 132.59 (out)(err) |
ram_k3_n10.ra1.wcnf | O = 232 T = 2.00 |
O = 232 T = 8.77 (out)(err) |
O = 232 T = 2.00 (out)(err) |
ram_k3_n11.ra1.wcnf | O = 318 T = 2.72 |
O = 318 T = 51.63 (out)(err) |
O = 318 T = 2.72 (out)(err) |
ram_k3_n12.ra1.wcnf | O = 524 T = 3.84 |
O = 524 T = 146.30 (out)(err) |
O = 524 T = 3.84 (out)(err) |
ram_k3_n13.ra1.wcnf | O = 1417 T = 4.21 |
O = 7966 T = 3.55 (out)(err) |
O = 1417 T = 4.21 (out)(err) |
ram_k3_n14.ra1.wcnf | O = 3025 T = 5.01 |
O = 10626 T = 1.36 (out)(err) |
O = 3025 T = 5.01 (out)(err) |
ram_k3_n15.ra1.wcnf | O = 4884 T = 3.52 |
O = 10976 T = 4.00 (out)(err) |
O = 4884 T = 3.52 (out)(err) |
ram_k3_n16.ra1.wcnf | O = 7271 T = 6.95 |
O = 16323 T = 1.72 (out)(err) |
O = 7271 T = 6.95 (out)(err) |
ram_k3_n17.ra1.wcnf | O = 10372 T = 7.97 |
O = 29190 T = 3.74 (out)(err) |
O = 10372 T = 7.97 (out)(err) |
ram_k3_n18.ra1.wcnf | O = 15621 T = 33.35 |
O = 36425 T = 3.78 (out)(err) |
O = 15621 T = 33.35 (out)(err) |
ram_k3_n19.ra1.wcnf | O = 20665 T = 10.30 |
O = 50874 T = 4.01 (out)(err) |
O = 20665 T = 10.30 (out)(err) |
ram_k3_n20.ra1.wcnf | O = 23898 T = 14.59 |
O = 56504 T = 3.48 (out)(err) |
O = 23898 T = 14.59 (out)(err) |
ram_k3_n9.ra1.wcnf | O = 7 T = 1.39 |
O = 7 T = 2.22 (out)(err) |
O = 7 T = 1.39 (out)(err) |
ram_k4_n18.ra1.wcnf | O = 460 T = 171.95 |
O = 12033 T = 7.12 (out)(err) |
O = 460 T = 171.95 (out)(err) |
ram_k4_n19.ra1.wcnf | O = 1508 T = 16.16 |
O = 16899 T = 4.45 (out)(err) |
O = 1508 T = 16.16 (out)(err) |
ram_k4_n20.ra1.wcnf | O = 3585 T = 67.69 |
O = 25022 T = 4.63 (out)(err) |
O = 3585 T = 67.69 (out)(err) |
MANN_a27.clq.wcnf | O = 2049 T = 2.23 |
O = 2202 T = 6.13 (out)(err) |
O = 2049 T = 2.23 (out)(err) |
MANN_a45.clq.wcnf | O = 2057 T = 1.12 |
O = 2221 T = 5.99 (out)(err) |
O = 2057 T = 1.12 (out)(err) |
MANN_a81.clq.wcnf | O = 1995 T = 2.65 |
O = 2136 T = 5.40 (out)(err) |
O = 1995 T = 2.65 (out)(err) |
MANN_a9.clq.wcnf | O = 2179 T = 2.49 |
O = 2320 T = 6.18 (out)(err) |
O = 2179 T = 2.49 (out)(err) |
brock200_1.clq.wcnf | O = 1254 T = 2.49 |
O = 1408 T = 6.70 (out)(err) |
O = 1254 T = 2.49 (out)(err) |
brock200_2.clq.wcnf | O = 753 T = 2.15 |
O = 844 T = 5.41 (out)(err) |
O = 753 T = 2.15 (out)(err) |
brock200_3.clq.wcnf | O = 1102 T = 1.94 |
O = 1285 T = 5.32 (out)(err) |
O = 1102 T = 1.94 (out)(err) |
brock200_4.clq.wcnf | O = 1105 T = 2.45 |
O = 1265 T = 5.90 (out)(err) |
O = 1105 T = 2.45 (out)(err) |
brock400_1.clq.wcnf | O = 1361 T = 2.54 |
O = 1502 T = 4.21 (out)(err) |
O = 1361 T = 2.54 (out)(err) |
brock400_2.clq.wcnf | O = 1355 T = 2.14 |
O = 1498 T = 2.77 (out)(err) |
O = 1355 T = 2.14 (out)(err) |
brock400_3.clq.wcnf | O = 1259 T = 2.83 |
O = 1395 T = 3.94 (out)(err) |
O = 1259 T = 2.83 (out)(err) |
brock400_4.clq.wcnf | O = 1290 T = 2.54 |
O = 1462 T = 8.10 (out)(err) |
O = 1290 T = 2.54 (out)(err) |
brock800_1.clq.wcnf | O = 1071 T = 2.30 |
O = 1232 T = 6.67 (out)(err) |
O = 1071 T = 2.30 (out)(err) |
brock800_2.clq.wcnf | O = 1076 T = 2.08 |
O = 1259 T = 4.07 (out)(err) |
O = 1076 T = 2.08 (out)(err) |
brock800_3.clq.wcnf | O = 1079 T = 2.55 |
O = 1210 T = 3.08 (out)(err) |
O = 1079 T = 2.55 (out)(err) |
brock800_4.clq.wcnf | O = 1050 T = 1.73 |
O = 1225 T = 6.08 (out)(err) |
O = 1050 T = 1.73 (out)(err) |
c-fat200-1.clq.wcnf | O = 14 T = 0.55 |
O = 14 T = 0.55 (out)(err) |
O = 14 T = 1.29 (out)(err) |
c-fat200-2.clq.wcnf | O = 167 T = 2.19 |
O = 215 T = 2.60 (out)(err) |
O = 167 T = 2.19 (out)(err) |
c-fat200-5.clq.wcnf | O = 613 T = 3.21 |
O = 753 T = 4.38 (out)(err) |
O = 613 T = 3.21 (out)(err) |
c-fat500-1.clq.wcnf | O = 10 T = 0.36 |
O = 10 T = 0.36 (out)(err) |
O = 10 T = 1.31 (out)(err) |
c-fat500-10.clq.wcnf | O = 947 T = 2.07 |
O = 1009 T = 1.73 (out)(err) |
O = 947 T = 2.07 (out)(err) |
c-fat500-2.clq.wcnf | O = 97 T = 1.12 |
O = 102 T = 4.36 (out)(err) |
O = 97 T = 1.12 (out)(err) |
c-fat500-5.clq.wcnf | O = 404 T = 1.39 |
O = 452 T = 4.95 (out)(err) |
O = 404 T = 1.39 (out)(err) |
hamming10-2.clq.wcnf | O = 1929 T = 2.51 |
O = 2104 T = 4.05 (out)(err) |
O = 1929 T = 2.51 (out)(err) |
hamming10-4.clq.wcnf | O = 1683 T = 2.34 |
O = 1812 T = 4.98 (out)(err) |
O = 1683 T = 2.34 (out)(err) |
hamming6-2.clq.wcnf | O = 4391 T = 3.02 |
O = 4732 T = 3.63 (out)(err) |
O = 4391 T = 3.02 (out)(err) |
hamming6-4.clq.wcnf | O = 1035 T = 2.51 |
O = 1483 T = 3.29 (out)(err) |
O = 1035 T = 2.51 (out)(err) |
hamming8-2.clq.wcnf | O = 2213 T = 2.86 |
O = 2319 T = 4.94 (out)(err) |
O = 2213 T = 2.86 (out)(err) |
hamming8-4.clq.wcnf | O = 917 T = 2.30 |
O = 1191 T = 6.94 (out)(err) |
O = 917 T = 2.30 (out)(err) |
johnson16-2-4.clq.wcnf | O = 1170 T = 2.10 |
O = 1396 T = 5.59 (out)(err) |
O = 1170 T = 2.10 (out)(err) |
johnson32-2-4.clq.wcnf | O = 1788 T = 2.35 |
O = 2030 T = 5.48 (out)(err) |
O = 1788 T = 2.35 (out)(err) |
johnson8-2-4.clq.wcnf | O = 392 T = 1.27 |
O = 444 T = 6.28 (out)(err) |
O = 392 T = 1.27 (out)(err) |
johnson8-4-4.clq.wcnf | O = 4154 T = 3.57 |
O = 4759 T = 6.55 (out)(err) |
O = 4154 T = 3.57 (out)(err) |
keller4.clq.wcnf | O = 1133 T = 2.38 |
O = 1398 T = 4.96 (out)(err) |
O = 1133 T = 2.38 (out)(err) |
keller5.clq.wcnf | O = 1383 T = 2.62 |
O = 1543 T = 4.61 (out)(err) |
O = 1383 T = 2.62 (out)(err) |
p_hat1000-1.clq.wcnf | O = 248 T = 1.87 |
O = 344 T = 4.80 (out)(err) |
O = 248 T = 1.87 (out)(err) |
p_hat1000-2.clq.wcnf | O = 752 T = 2.15 |
O = 802 T = 0.56 (out)(err) |
O = 752 T = 2.15 (out)(err) |
p_hat1000-3.clq.wcnf | O = 1251 T = 1.83 |
O = 1451 T = 4.89 (out)(err) |
O = 1251 T = 1.83 (out)(err) |
p_hat300-1.clq.wcnf | O = 243 T = 2.10 |
O = 296 T = 6.42 (out)(err) |
O = 243 T = 2.10 (out)(err) |
p_hat300-2.clq.wcnf | O = 711 T = 1.75 |
O = 850 T = 4.08 (out)(err) |
O = 711 T = 1.75 (out)(err) |
p_hat300-3.clq.wcnf | O = 1439 T = 2.29 |
O = 1616 T = 5.85 (out)(err) |
O = 1439 T = 2.29 (out)(err) |
p_hat500-1.clq.wcnf | O = 395 T = 1.93 |
O = 496 T = 5.22 (out)(err) |
O = 395 T = 1.93 (out)(err) |
p_hat500-2.clq.wcnf | O = 931 T = 2.14 |
O = 1006 T = 4.14 (out)(err) |
O = 931 T = 2.14 (out)(err) |
p_hat500-3.clq.wcnf | O = 1501 T = 2.84 |
O = 1679 T = 6.41 (out)(err) |
O = 1501 T = 2.84 (out)(err) |
p_hat700-1.clq.wcnf | O = 329 T = 1.66 |
O = 390 T = 4.90 (out)(err) |
O = 329 T = 1.66 (out)(err) |
p_hat700-2.clq.wcnf | O = 834 T = 2.26 |
O = 905 T = 2.63 (out)(err) |
O = 834 T = 2.26 (out)(err) |
p_hat700-3.clq.wcnf | O = 1432 T = 0.43 |
O = 1625 T = 4.42 (out)(err) |
O = 1432 T = 0.43 (out)(err) |
san1000.clq.wcnf | O = 744 T = 2.61 |
O = 840 T = 2.96 (out)(err) |
O = 744 T = 2.61 (out)(err) |
san200_0.7_1.clq.wcnf | O = 1256 T = 3.07 |
O = 1422 T = 4.51 (out)(err) |
O = 1256 T = 3.07 (out)(err) |
san200_0.7_2.clq.wcnf | O = 1243 T = 1.95 |
O = 1446 T = 5.57 (out)(err) |
O = 1243 T = 1.95 (out)(err) |
san200_0.9_1.clq.wcnf | O = 1672 T = 2.94 |
O = 1778 T = 5.94 (out)(err) |
O = 1672 T = 2.94 (out)(err) |
san200_0.9_2.clq.wcnf | O = 1647 T = 3.24 |
O = 1769 T = 3.39 (out)(err) |
O = 1647 T = 3.24 (out)(err) |
san200_0.9_3.clq.wcnf | O = 1670 T = 2.16 |
O = 1830 T = 9.82 (out)(err) |
O = 1670 T = 2.16 (out)(err) |
san400_0.5_1.clq.wcnf | O = 718 T = 2.24 |
O = 962 T = 2.29 (out)(err) |
O = 718 T = 2.24 (out)(err) |
san400_0.7_1.clq.wcnf | O = 1258 T = 2.04 |
O = 1359 T = 5.94 (out)(err) |
O = 1258 T = 2.04 (out)(err) |
san400_0.7_2.clq.wcnf | O = 1237 T = 2.36 |
O = 1357 T = 1.88 (out)(err) |
O = 1237 T = 2.36 (out)(err) |
san400_0.7_3.clq.wcnf | O = 1201 T = 2.33 |
O = 1408 T = 2.12 (out)(err) |
O = 1201 T = 2.33 (out)(err) |
san400_0.9_1.clq.wcnf | O = 1604 T = 1.35 |
O = 1767 T = 4.96 (out)(err) |
O = 1604 T = 1.35 (out)(err) |
sanr200_0.7.clq.wcnf | O = 1171 T = 2.57 |
O = 1389 T = 4.66 (out)(err) |
O = 1171 T = 2.57 (out)(err) |
sanr200_0.9.clq.wcnf | O = 1610 T = 1.98 |
O = 1743 T = 2.97 (out)(err) |
O = 1610 T = 1.98 (out)(err) |
sanr400_0.5.clq.wcnf | O = 763 T = 2.43 |
O = 991 T = 6.37 (out)(err) |
O = 763 T = 2.43 (out)(err) |
sanr400_0.7.clq.wcnf | O = 1198 T = 2.30 |
O = 1328 T = 4.38 (out)(err) |
O = 1198 T = 2.30 (out)(err) |
t3g3-5555.spn.wcnf | O = 1100610 T = 1.14 |
O = 1190133 T = 4.53 (out)(err) |
O = 1100610 T = 1.14 (out)(err) |
t4g3-6666.spn.wcnf | O = 2275606 T = 3.47 |
O = 3111368 T = 6.41 (out)(err) |
O = 2275606 T = 3.47 (out)(err) |
t5g3-7777.spn.wcnf | O = 4241951 T = 6.57 |
O = 5056683 T = 6.51 (out)(err) |
O = 4241951 T = 6.57 (out)(err) |
t6g3-8888.spn.wcnf | O = 7844119 T = 140.99 |
O = 10552689 T = 5.37 (out)(err) |
O = 7844119 T = 140.99 (out)(err) |
t7g3-9999.spn.wcnf | O = 11957389 T = 156.79 |
O = 15917405 T = 1.90 (out)(err) |
O = 11957389 T = 156.79 (out)(err) |