| 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 | ISAC+-2016-in |
|---|---|---|
| rsdecoder-debug.dimacs.cnf | O = 1 T = 11.55 |
O = 1 T = 11.55 |
| sudoku-debug.dimacs.cnf | O = 1 T = 11.44 |
O = 1 T = 11.44 |
| wb-debug.dimacs.cnf | O = 28 T = 8.63 |
O = 28 T = 8.63 |
| SM_AS_TOP_buggy1.dimacs.filtered.cnf | O = 57 T = 50.73 |
O = 57 T = 50.73 |
| SM_MAIN_MEM_buggy1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| SM_RX_TOP.dimacs.filtered.cnf | O = 6 T = 17.51 |
O = 6 T = 17.51 |
| b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 9.89 |
O = 4 T = 9.89 |
| c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 8.06 |
O = 4 T = 8.06 |
| c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 11.26 |
O = 4 T = 11.26 |
| c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 10.75 |
O = 8 T = 10.75 |
| c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 8.61 |
O = 4 T = 8.61 |
| c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 7.85 |
O = 8 T = 7.85 |
| c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 7.82 |
O = 8 T = 7.82 |
| c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 7.46 |
O = 8 T = 7.46 |
| divider-problem.dimacs_11.filtered.cnf | O = 2 T = 62.35 |
O = 2 T = 62.35 |
| divider-problem.dimacs_2.filtered.cnf | O = 2 T = 55.35 |
O = 2 T = 55.35 |
| divider-problem.dimacs_5.filtered.cnf | O = 2 T = 61.56 |
O = 2 T = 61.56 |
| divider-problem.dimacs_8.filtered.cnf | O = 2 T = 39.44 |
O = 2 T = 39.44 |
| dividers10.dimacs.filtered.cnf | O = 2 T = 9.09 |
O = 2 T = 9.09 |
| dividers_multivec1.dimacs.filtered.cnf | O = 2 T = 8.79 |
O = 2 T = 8.79 |
| fpu_multivec1-problem.dimacs_14.filtered.cnf | O = 2 T = 10.61 |
O = 2 T = 10.61 |
| i2c-problem.dimacs_25.filtered.cnf | O = 2 T = 19.65 |
O = 2 T = 19.65 |
| i2c-problem.dimacs_26.filtered.cnf | O = 2 T = 31.84 |
O = 2 T = 31.84 |
| mem_ctrl-problem.dimacs_27.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| mem_ctrl1.dimacs.filtered.cnf | O = 1 T = 19.71 |
O = 1 T = 19.71 |
| mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| mrisc_mem2wire-problem.dimacs_29.filtered.cnf | O = 1 T = 16.83 |
O = 1 T = 16.83 |
| rsdecoder-problem.dimacs_31.filtered.cnf | O = 3 T = 21.67 |
O = 3 T = 21.67 |
| rsdecoder-problem.dimacs_36.filtered.cnf | O = 1 T = 13.42 |
O = 1 T = 13.42 |
| rsdecoder-problem.dimacs_37.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| rsdecoder-problem.dimacs_38.filtered.cnf | O = 2 T = 14.07 |
O = 2 T = 14.07 |
| rsdecoder-problem.dimacs_39.filtered.cnf | O = 1 T = 11.70 |
O = 1 T = 11.70 |
| rsdecoder-problem.dimacs_40.filtered.cnf | O = 1 T = 14.50 |
O = 1 T = 14.50 |
| rsdecoder-problem.dimacs_41.filtered.cnf | O = 2 T = 35.56 |
O = 2 T = 35.56 |
| rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf | O = 4 T = 276.41 |
O = 4 T = 276.41 |
| rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| rsdecoder2.dimacs.filtered.cnf | O = 1 T = 50.48 |
O = 1 T = 50.48 |
| rsdecoder4.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| rsdecoder5.dimacs.filtered.cnf | O = 2 T = 151.24 |
O = 2 T = 151.24 |
| rsdecoder6.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| rsdecoder_fsm2.dimacs.filtered.cnf | O = 2 T = 22.01 |
O = 2 T = 22.01 |
| rsdecoder_multivec1-problem.dimacs_33.filtered.cnf | O = 4 T = 79.40 |
O = 4 T = 79.40 |
| rsdecoder_multivec1.dimacs.filtered.cnf | O = 4 T = 9.95 |
O = 4 T = 9.95 |
| wb-problem.dimacs_45.filtered.cnf | O = 14 T = 8.70 |
O = 14 T = 8.70 |
| wb-problem.dimacs_46.filtered.cnf | O = 476 T = 27.69 |
O = 476 T = 27.69 |
| wb1.dimacs.filtered.cnf | O = 218 T = 7.97 |
O = 218 T = 7.97 |
| wb2.dimacs.filtered.cnf | O = 588 T = 12.50 |
O = 588 T = 12.50 |
| wb_4m8s-problem.dimacs_47.filtered.cnf | O = 34 T = 26.50 |
O = 34 T = 26.50 |
| wb_4m8s-problem.dimacs_48.filtered.cnf | O = 19 T = 26.61 |
O = 19 T = 26.61 |
| wb_4m8s-problem.dimacs_49.filtered.cnf | O = 230 T = 25.19 |
O = 230 T = 25.19 |
| wb_4m8s1.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| wb_4m8s3.dimacs.filtered.cnf | O = 8 T = 11.85 |
O = 8 T = 11.85 |
| wb_4m8s4.dimacs.filtered.cnf | O = N/A T = TO |
O = N/A T = TO |
| wb_conmax1.dimacs.filtered.cnf | O = 40 T = 185.80 |
O = 40 T = 185.80 |
| wb_conmax3.dimacs.filtered.cnf | O = 33 T = 20.09 |
O = 33 T = 20.09 |