| 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 | CCLS | SAT4Jms-ext-i | SAT4Jms-int-i | iraNovelty++ | optimax-it |
|---|---|---|---|---|---|---|
| rsdecoder-debug.dimacs.cnf | O = 1 T = 80.91 |
O = 399795 T = 1.96 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 80.91 (out)(err) |
| sudoku-debug.dimacs.cnf | O = 1 T = 9.79 |
O = 301652 T = 1.50 (out)(err) |
O = 1 T = 24.81 (out)(err) |
O = 1 T = 24.04 (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 9.79 (out)(err) |
| wb-debug.dimacs.cnf | O = 28 T = 2.36 |
O = 129488 T = 0.55 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 28 T = 2.36 (out)(err) |
| SM_AS_TOP_buggy1.dimacs.filtered.cnf | O = 156 T = 46.83 |
O = 107897 T = 0.47 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 156 T = 46.83 (out)(err) |
| SM_MAIN_MEM_buggy1.dimacs.filtered.cnf | O = 497 T = 84.32 |
O = 601585 T = 4.70 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 497 T = 84.32 (out)(err) |
| SM_RX_TOP.dimacs.filtered.cnf | O = 6 T = 80.54 |
O = 149686 T = 0.67 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6 T = 80.54 (out)(err) |
| b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 13.28 |
O = 369009 T = 1.42 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4 T = 13.28 (out)(err) |
| c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 1.55 |
O = 224410 T = 1.08 (out)(err) |
O = 4 T = 27.91 (out)(err) |
O = 4 T = 29.48 (out)(err) |
O = N/A T = TO (out)(err) |
O = 4 T = 1.55 (out)(err) |
| c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 81.46 |
O = 231068 T = 1.03 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4 T = 81.46 (out)(err) |
| c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 5.04 |
O = 478123 T = 1.76 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 8 T = 5.04 (out)(err) |
| c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf | O = 4 T = 2.86 |
O = 270013 T = 0.91 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4 T = 2.86 (out)(err) |
| c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 1.85 |
O = 113386 T = 0.42 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 8 T = 1.85 (out)(err) |
| c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 1.37 |
O = 112762 T = 0.41 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 8 T = 1.37 (out)(err) |
| c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf | O = 8 T = 2.59 |
O = 174385 T = 0.76 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 8 T = 2.59 (out)(err) |
| divider-problem.dimacs_11.filtered.cnf | O = 2 T = 42.02 |
O = 127614 T = 0.56 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 42.02 (out)(err) |
| divider-problem.dimacs_2.filtered.cnf | O = 8 T = 29.63 |
O = 136460 T = 0.56 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 8 T = 29.63 (out)(err) |
| divider-problem.dimacs_5.filtered.cnf | O = 2 T = 199.62 |
O = 136497 T = 0.56 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 199.62 (out)(err) |
| divider-problem.dimacs_8.filtered.cnf | O = 2 T = 15.08 |
O = 146536 T = 0.64 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 15.08 (out)(err) |
| dividers10.dimacs.filtered.cnf | O = 2 T = 4.40 |
O = 28100 T = 0.16 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 4.40 (out)(err) |
| dividers_multivec1.dimacs.filtered.cnf | O = 2 T = 4.23 |
O = 65768 T = 0.27 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 4.23 (out)(err) |
| fpu_multivec1-problem.dimacs_14.filtered.cnf | O = 2 T = 2.36 |
O = 159326 T = 0.77 (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 132.70 (out)(err) |
O = N/A T = TO (out)(err) |
O = 2 T = 2.36 (out)(err) |
| i2c-problem.dimacs_25.filtered.cnf | O = 1941 T = 14.20 |
O = 309430 T = 1.36 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1941 T = 14.20 (out)(err) |
| i2c-problem.dimacs_26.filtered.cnf | O = 4 T = 1.70 |
O = 236409 T = 0.89 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4 T = 1.70 (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) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| mem_ctrl1.dimacs.filtered.cnf | O = 1 T = 6.52 |
O = 747983 T = 3.71 (out)(err) |
O = 1 T = 125.73 (out)(err) |
O = 1 T = 38.98 (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 6.52 (out)(err) |
| mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf | O = 1183954 T = 6.97 |
O = 1183954 T = 6.97 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| mrisc_mem2wire-problem.dimacs_29.filtered.cnf | O = 1 T = 6.96 |
O = 508720 T = 2.23 (out)(err) |
O = 1 T = 27.89 (out)(err) |
O = 1 T = 27.16 (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 6.96 (out)(err) |
| rsdecoder-problem.dimacs_31.filtered.cnf | O = 692762 T = 4.03 |
O = 692762 T = 4.03 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_36.filtered.cnf | O = 1 T = 6.29 |
O = 705765 T = 3.56 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 6.29 (out)(err) |
| rsdecoder-problem.dimacs_37.filtered.cnf | O = 875564 T = 4.69 |
O = 875564 T = 4.69 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder-problem.dimacs_38.filtered.cnf | O = 48 T = 4.37 |
O = 691819 T = 3.37 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 48 T = 4.37 (out)(err) |
| rsdecoder-problem.dimacs_39.filtered.cnf | O = 1 T = 7.85 |
O = 693776 T = 3.95 (out)(err) |
O = 1 T = 63.90 (out)(err) |
O = 1 T = 64.01 (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 7.85 (out)(err) |
| rsdecoder-problem.dimacs_40.filtered.cnf | O = 1 T = 49.15 |
O = 705824 T = 2.84 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1 T = 49.15 (out)(err) |
| rsdecoder-problem.dimacs_41.filtered.cnf | O = 55 T = 4.47 |
O = 685117 T = 2.81 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 55 T = 4.47 (out)(err) |
| rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf | O = 6 T = 45.05 |
O = 144268 T = 0.80 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6 T = 45.05 (out)(err) |
| rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf | O = 478 T = 85.25 |
O = 199083 T = 1.06 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 478 T = 85.25 (out)(err) |
| rsdecoder2.dimacs.filtered.cnf | O = 259167 T = 1.72 |
O = 259167 T = 1.72 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder4.dimacs.filtered.cnf | O = 148116 T = 0.66 |
O = 148116 T = 0.66 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| rsdecoder5.dimacs.filtered.cnf | O = 23 T = 1.59 |
O = 148095 T = 0.75 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 23 T = 1.59 (out)(err) |
| rsdecoder6.dimacs.filtered.cnf | O = 1673 T = 66.19 |
O = 149432 T = 1.03 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1673 T = 66.19 (out)(err) |
| rsdecoder_fsm2.dimacs.filtered.cnf | O = 904 T = 191.02 |
O = 149672 T = 0.67 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 904 T = 191.02 (out)(err) |
| rsdecoder_multivec1-problem.dimacs_33.filtered.cnf | O = 4 T = 15.55 |
O = 363861 T = 2.25 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4 T = 15.55 (out)(err) |
| rsdecoder_multivec1.dimacs.filtered.cnf | O = 245702 T = 1.19 |
O = 245702 T = 1.19 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb-problem.dimacs_45.filtered.cnf | O = 14 T = 1.36 |
O = 169883 T = 0.65 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 14 T = 1.36 (out)(err) |
| wb-problem.dimacs_46.filtered.cnf | O = 476 T = 16.76 |
O = 165614 T = 0.72 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 476 T = 16.76 (out)(err) |
| wb1.dimacs.filtered.cnf | O = 218 T = 1.53 |
O = 29911 T = 0.11 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 218 T = 1.53 (out)(err) |
| wb2.dimacs.filtered.cnf | O = 588 T = 3.90 |
O = 1127 T = 229.89 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 588 T = 3.90 (out)(err) |
| wb_4m8s-problem.dimacs_47.filtered.cnf | O = 1551204 T = 8.53 |
O = 1551204 T = 8.53 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb_4m8s-problem.dimacs_48.filtered.cnf | O = 1594424 T = 6.44 |
O = 1594424 T = 6.44 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb_4m8s-problem.dimacs_49.filtered.cnf | O = 1603369 T = 8.39 |
O = 1603369 T = 8.39 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| wb_4m8s1.dimacs.filtered.cnf | O = 29 T = 144.46 |
O = 287318 T = 2.25 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 29 T = 144.46 (out)(err) |
| wb_4m8s3.dimacs.filtered.cnf | O = 8 T = 2.73 |
O = 288573 T = 1.21 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 8 T = 2.73 (out)(err) |
| wb_4m8s4.dimacs.filtered.cnf | O = 225 T = 85.98 |
O = 286777 T = 1.38 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 225 T = 85.98 (out)(err) |
| wb_conmax1.dimacs.filtered.cnf | O = 41 T = 22.61 |
O = 182632 T = 1.06 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 41 T = 22.61 (out)(err) |
| wb_conmax3.dimacs.filtered.cnf | O = 35 T = 48.49 |
O = 182619 T = 0.98 (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 35 T = 48.49 (out)(err) |