| 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 |
|---|---|---|---|
| rsdecoder-debug.dimacs.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 317050 T = 261.02 (out)(err) |
| sudoku-debug.dimacs.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 2 T = 269.06 (out)(err) |
| wb-debug.dimacs.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 3971 T = 223.19 (out)(err) |
| SM_AS_TOP_buggy1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 5 T = 150.73 (out)(err) |
| SM_MAIN_MEM_buggy1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| SM_RX_TOP.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 2 T = 191.17 (out)(err) |
| b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 24306 T = 251.92 (out)(err) |
| c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 108 T = 226.10 (out)(err) |
| c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 11040 T = 227.53 (out)(err) |
| c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 3846 T = 257.28 (out)(err) |
| c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 161930 T = 232.62 (out)(err) |
| c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = 16 T = 58.95 (out)(err) |
O = 1 T = 209.81 (out)(err) |
| c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = 16 T = 60.98 (out)(err) |
O = 1 T = 218.76 (out)(err) |
| c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 55405 T = 203.56 (out)(err) |
| divider-problem.dimacs_11.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 18266 T = 217.92 (out)(err) |
| divider-problem.dimacs_2.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 23416 T = 209.61 (out)(err) |
| divider-problem.dimacs_5.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 25762 T = 210.36 (out)(err) |
| divider-problem.dimacs_8.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 29868 T = 203.80 (out)(err) |
| dividers10.dimacs.filtered.cnf | O = 4 T = 7.83 |
O = 4 T = 7.83 (out)(err) |
O = 1264 T = 248.01 (out)(err) |
| dividers_multivec1.dimacs.filtered.cnf | O = 5 T = 20.39 |
O = 5 T = 20.39 (out)(err) |
O = 5070 T = 188.37 (out)(err) |
| fpu_multivec1-problem.dimacs_14.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 33348 T = 202.21 (out)(err) |
| i2c-problem.dimacs_25.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 193548 T = 230.18 (out)(err) |
| i2c-problem.dimacs_26.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 112027 T = 227.48 (out)(err) |
| mem_ctrl-problem.dimacs_27.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| mem_ctrl1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| mrisc_mem2wire-problem.dimacs_29.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_31.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_36.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_37.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_38.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_39.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_40.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_41.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 34573 T = 213.35 (out)(err) |
| rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 11 T = 250.85 (out)(err) |
| rsdecoder2.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 122496 T = 238.95 (out)(err) |
| rsdecoder4.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 28198 T = 216.70 (out)(err) |
| rsdecoder5.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 296 T = 216.06 (out)(err) |
| rsdecoder6.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 30211 T = 213.92 (out)(err) |
| rsdecoder_fsm2.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 28586 T = 211.83 (out)(err) |
| rsdecoder_multivec1-problem.dimacs_33.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 245045 T = 245.86 (out)(err) |
| rsdecoder_multivec1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 10711 T = 225.10 (out)(err) |
| wb-problem.dimacs_45.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 5 T = 217.09 (out)(err) |
| wb-problem.dimacs_46.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 53056 T = 214.47 (out)(err) |
| wb1.dimacs.filtered.cnf | O = N/A T = TO |
O = 453 T = 5.99 (out)(err) |
O = 1020 T = 112.71 (out)(err) |
| wb2.dimacs.filtered.cnf | O = N/A T = TO |
O = 793 T = 9.46 (out)(err) |
O = 1543 T = 101.52 (out)(err) |
| wb_4m8s-problem.dimacs_47.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb_4m8s-problem.dimacs_48.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb_4m8s-problem.dimacs_49.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb_4m8s1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 156700 T = 236.45 (out)(err) |
| wb_4m8s3.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 1 T = 237.30 (out)(err) |
| wb_4m8s4.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 157331 T = 239.23 (out)(err) |
| wb_conmax1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 53733 T = 205.14 (out)(err) |
| wb_conmax3.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = 497 T = 209.52 (out)(err) |