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 ISAC+-2016-co
rsdecoder-debug.dimacs.cnf S = OPT
O = 1
T = 19.25		 S = OPT
O = 1
T = 19.25
sudoku-debug.dimacs.cnf S = OPT
O = 1
T = 7.79		 S = OPT
O = 1
T = 7.79
wb-debug.dimacs.cnf S = OPT
O = 28
T = 7.52		 S = OPT
O = 28
T = 7.52
SM_AS_TOP_buggy1.dimacs.filtered.cnf S = OPT
O = 57
T = 53.46		 S = OPT
O = 57
T = 53.46
SM_MAIN_MEM_buggy1.dimacs.filtered.cnf S = OPT
O = 390
T = 363.87		 S = OPT
O = 390
T = 363.87
SM_RX_TOP.dimacs.filtered.cnf S = OPT
O = 6
T = 16.05		 S = OPT
O = 6
T = 16.05
b15-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 8.89		 S = OPT
O = 4
T = 8.89
c1_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 5.94		 S = OPT
O = 4
T = 5.94
c2_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 8.03		 S = OPT
O = 4
T = 8.03
c4_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 8.88		 S = OPT
O = 8
T = 8.88
c4_DD_s3_f1_e2_v1-bug-fourvec-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 4
T = 6.44		 S = OPT
O = 4
T = 6.44
c5_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 5.07		 S = OPT
O = 8
T = 5.07
c5_DD_s3_f1_e1_v2-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 5.06		 S = OPT
O = 8
T = 5.06
c6_DD_s3_f1_e1_v1-bug-gate-0.dimacs.seq.filtered.cnf S = OPT
O = 8
T = 5.77		 S = OPT
O = 8
T = 5.77
divider-problem.dimacs_11.filtered.cnf S = OPT
O = 2
T = 11.29		 S = OPT
O = 2
T = 11.29
divider-problem.dimacs_2.filtered.cnf S = OPT
O = 2
T = 34.81		 S = OPT
O = 2
T = 34.81
divider-problem.dimacs_5.filtered.cnf S = OPT
O = 2
T = 17.03		 S = OPT
O = 2
T = 17.03
divider-problem.dimacs_8.filtered.cnf S = OPT
O = 2
T = 39.01		 S = OPT
O = 2
T = 39.01
dividers10.dimacs.filtered.cnf S = OPT
O = 2
T = 4.73		 S = OPT
O = 2
T = 4.73
dividers_multivec1.dimacs.filtered.cnf S = OPT
O = 2
T = 6.05		 S = OPT
O = 2
T = 6.05
fpu_multivec1-problem.dimacs_14.filtered.cnf S = OPT
O = 2
T = 8.62		 S = OPT
O = 2
T = 8.62
i2c-problem.dimacs_25.filtered.cnf S = OPT
O = 2
T = 11.30		 S = OPT
O = 2
T = 11.30
i2c-problem.dimacs_26.filtered.cnf S = OPT
O = 2
T = 11.48		 S = OPT
O = 2
T = 11.48
mem_ctrl-problem.dimacs_27.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
mem_ctrl1.dimacs.filtered.cnf S = OPT
O = 1
T = 18.23		 S = OPT
O = 1
T = 18.23
mem_ctrl2_blackbox_mc_dp-problem.dimacs_28.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
mrisc_mem2wire-problem.dimacs_29.filtered.cnf S = OPT
O = 1
T = 10.55		 S = OPT
O = 1
T = 10.55
rsdecoder-problem.dimacs_31.filtered.cnf S = OPT
O = 1
T = 36.05		 S = OPT
O = 1
T = 36.05
rsdecoder-problem.dimacs_36.filtered.cnf S = OPT
O = 1
T = 30.69		 S = OPT
O = 1
T = 30.69
rsdecoder-problem.dimacs_37.filtered.cnf S = OPT
O = 1
T = 19.28		 S = OPT
O = 1
T = 19.28
rsdecoder-problem.dimacs_38.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rsdecoder-problem.dimacs_39.filtered.cnf S = OPT
O = 1
T = 12.94		 S = OPT
O = 1
T = 12.94
rsdecoder-problem.dimacs_40.filtered.cnf S = OPT
O = 1
T = 46.41		 S = OPT
O = 1
T = 46.41
rsdecoder-problem.dimacs_41.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
rsdecoder1_blackbox_CSEEblock-problem.dimacs_32.filtered.cnf S = OPT
O = 4
T = 269.20		 S = OPT
O = 4
T = 269.20
rsdecoder1_blackbox_KESblock-problem.dimacs_30.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 1710.39
rsdecoder2.dimacs.filtered.cnf S = OPT
O = 1
T = 15.94		 S = OPT
O = 1
T = 15.94
rsdecoder4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = 1187.01
rsdecoder5.dimacs.filtered.cnf S = OPT
O = 2
T = 25.64		 S = OPT
O = 2
T = 25.64
rsdecoder6.dimacs.filtered.cnf S = OPT
O = 3
T = 325.76		 S = OPT
O = 3
T = 325.76
rsdecoder_fsm2.dimacs.filtered.cnf S = OPT
O = 2
T = 9.41		 S = OPT
O = 2
T = 9.41
rsdecoder_multivec1-problem.dimacs_33.filtered.cnf S = OPT
O = 4
T = 39.59		 S = OPT
O = 4
T = 39.59
rsdecoder_multivec1.dimacs.filtered.cnf S = OPT
O = 4
T = 21.21		 S = OPT
O = 4
T = 21.21
wb-problem.dimacs_45.filtered.cnf S = OPT
O = 14
T = 5.72		 S = OPT
O = 14
T = 5.72
wb-problem.dimacs_46.filtered.cnf S = OPT
O = 476
T = 19.98		 S = OPT
O = 476
T = 19.98
wb1.dimacs.filtered.cnf S = OPT
O = 218
T = 5.24		 S = OPT
O = 218
T = 5.24
wb2.dimacs.filtered.cnf S = OPT
O = 588
T = 7.43		 S = OPT
O = 588
T = 7.43
wb_4m8s-problem.dimacs_47.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
wb_4m8s-problem.dimacs_48.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
wb_4m8s-problem.dimacs_49.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
wb_4m8s1.dimacs.filtered.cnf S = OPT
O = 18
T = 537.40		 S = OPT
O = 18
T = 537.40
wb_4m8s3.dimacs.filtered.cnf S = OPT
O = 8
T = 9.95		 S = OPT
O = 8
T = 9.95
wb_4m8s4.dimacs.filtered.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
wb_conmax1.dimacs.filtered.cnf S = OPT
O = 40
T = 40.90		 S = OPT
O = 40
T = 40.90
wb_conmax3.dimacs.filtered.cnf S = OPT
O = 33
T = 16.13		 S = OPT
O = 33
T = 16.13