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 |