Benchmark

LabelMeaning
SSolution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time (TO for Time Out)
(out)(err)Standard output and standard error for each solver

ColorMeaning for Complete SolversMeaning for Incomplete Solvers
TextBest solver columnBest solver column
TextOptimal solution with the best CPU timeBest solution with the best CPU time
TextOptimal solution and finished within the Time OutBest solution without the best CPU time
TextOptimal solution and did not finish within the Time OutSolution found but not the best
TextTime OutTime Out
TextBuggy solutionBuggy 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)