PBSugar: Experimental Results

Overview
Machine Specification and Software Versions
Benchmark Instances
Results on Solving
Raw Data
- Table of PBSugar Raw Data
References

Overview

This web page reports the experimental results of PBSugar version 1.1 for all 669 instances of DEC-SMALLINT-LIN (decision problems, small integers, linear constraints) category of 2011 PB competition benchmark set. The following solvers are executed on our environment.


Name	Description	Reference
PBSugar	PBSugar version 1.1
Sat4j	Sat4j PB Res//CP version 2.3.2	Le Berre and Parrain {BerreP10}
clasp	clasp version 2.1.1 (64-bit code)	Gebser et al. {GebserKNS07}
bsolo	bsolo version 3.2 (32-bit code)	Manquinho and Silva {ManquinhoS06}
wbo	wbo version 1.4a (32-bit code)	Manquinho et al. {ManquinhoML10}
MiniSat+	MiniSat+ version 1.0 (64-bit code)	Eén and Sörensson {EenS06}

Sat4j PB Rees//CP version 2.3.2 was ranked first in 2012 PB competition DEC-SMALLINT-LIN category.
clasp version 2.1.1 is a newer version of clasp version 2.0.6 which was ranked second as the submitted solver in 2012 PB competition DEC-SMALLINT-LIN category.
bsolo version 3.2 was ranked third in 2010 PB competition DEC-SMALLINT-LIN category, and its 32-bit binary code is avaiable from 2010 PB competition site.
wbo version 1.4a was ranked fourth in 2010 PB competition DEC-SMALLINT-LIN category, and its 32-bit binary code is avaiable from 2010 PB competition site.
MiniSat+ version 1.0 was ranked third in 2006 PB competition SATUNSAT-SMALLINT category, and its source code is avaiable from MiniSat+ site.
See http://www.cril.univ-artois.fr/PB12/results/ranking.php?idev=67 for the ranking in 2012 PB competition DEC-SMALLINT-LIN category.

Machine Specification and Software Versions

CPU: Intel Dual Core Xeon X5260 (L2 cache 6MB) 3.33GHz x 2 (6650 bogomips)
Memory: 16GB (4 x 4GB DDR2 SDRAM)
OS: Linux kernel version 3.2.0 generic x86_64 (Ubuntu Linux 12.04)
Java: Java version 1.6.0_27, OpenJDK Runtime Environment
Glucose version 2.1 with SatELite preprocessor (64 bit code)
PBSugar version 1.1.1 with default encoding options:
- sort=d : sort terms with the descending order of coefficients
- clause : extract clause part from PB constraint
- cnf=3 : translate directly to CNF by order encoding for the PB constraints containing at most 3 literals
- decomp=100 : try decomposition of PB constraints for the base up to 100
- axioms : generate axiom clauses
- cache : use "reusing cache" of counter matrices
- share=4 : try to share counter matrices when the length is greater than or equal to 4

Benchmark Instances

Download pb-dsl-list.csv.
- NAME : Name of the instance
- FAMILY : Name of the family
- VARS : Number of variables
- PBS : Number of PB constraints
- FILE : File name of the instance


Family	#Instances	Avg #Vars	Avg #Constraints
lopes	200	47539	1095387
army	12	348	643
blast	8	3760	7763
cache	9	63418	185607
chnl	21	2290	125
dbstv30	5	1600	328901
dbstv40	5	2800	990001
dbstv50	5	4500	2559501
dlx	3	7674	21764
elf	5	16593	47846
fpga	36	933	687
j120	28	31469	104663
j30	17	4296	13955
j60	18	9550	31142
j90	17	15524	50891
neos	4	5846	5283
ooo	19	34768	99704
pig-card	20	4015	113
pig-cl	20	4015	161208
ppp	6	4629	30870
robin	6	8876	761
13queen	100	169	101
11tsp11	100	231	2707
vdw	5	2472	276818
Total		19003	376878

There are 669 instances in 22 families. The family classification is given by {AbioNORM12}.
The following 7 instances are included in "lopes" family as classified in {AbioNORM12}.
- normalized-1096.cudf.paranoid.opb
- normalized-22s.smv.opb lopes
- normalized-25s.smv.opb lopes
- normalized-37s.smv.opb lopes
- normalized-43s.smv.opb lopes
- normalized-44s.smv.opb lopes
- normalized-46s.smv.opb lopes
The name of 5 instances are renamed as used in {AbioNORM12}.
- normalized-ppp:1,3-13,19.opb is renamed to normalized-ppp1-3-13-19.opb.
- normalized-ppp:1-11,19,21.opb is renmaed to normalized-ppp1-11-19-21.opb.
- normalized-ppp:1-12,16.opb is renmaed to normalized-ppp1-12-16.opb.
- normalized-ppp:1-9,16-19.opb is renmaed to normalized-ppp1-9-16-19.opb.
- normalized-ppp:3-13,25,26.opb is renmaed to normalized-ppp3-13-25-26.opb.

Results on Solving

Number of instances solved


Family	VBS	PBSugar	Sat4j	clasp	bsolo	wbo	MiniSat+
lopes (200)	86	81	44	67	36	65	64
army (12)	11	8	5	10	6	5	6
blast (8)	8	8	8	8	8	8	8
cache (9)	9	9	6	9	6	6	8
chnl (21)	21	6	21	3	21	3	3
dbstv30 (5)	5	5	5	5	5	5	5
dbstv40 (5)	5	5	5	5	5	5	5
dbstv50 (5)	5	5	5	5	5	5	5
dlx (3)	3	3	3	3	3	3	3
elf (5)	5	5	5	5	5	5	5
fpga (36)	36	36	36	34	36	36	33
j120 (28)	16	15	15	16	13	15	12
j30 (17)	17	17	17	17	17	17	17
j60 (18)	17	17	17	17	17	17	17
j90 (17)	17	17	17	17	17	17	17
neos (4)	2	2	2	2	2	2	2
ooo (19)	18	15	15	17	12	16	16
pig-card (20)	20	2	20	2	19	2	2
pig-cl (20)	2	2	2	2	2	2	2
ppp (6)	5	4	4	3	4	3	4
robin (6)	4	3	4	4	3	3	3
13queen (100)	100	100	100	100	100	100	100
11tsp11 (100)	100	100	100	100	85	100	95
vdw (5)	3	2	1	2	1	1	1
Total (669)	515	467	457	453	428	441	433

This table shows the number of solved instances within the time limit (1000 seconds).

Time spent for solving


Family	VBS	PBSugar	Sat4j	clasp	bsolo	wbo	MiniSat+
lopes (200)	638	657	844	727	847	746	752
army (12)	218	359	603	281	565	638	506
blast (8)	0	83	1	0	0	0	0
cache (9)	117	141	346	164	395	338	221
chnl (21)	0	761	1	863	0	892	861
dbstv30 (5)	1	18	6	8	24	1	8
dbstv40 (5)	2	45	12	47	163	2	13
dbstv50 (5)	6	107	29	123	187	6	102
dlx (3)	0	6	3	0	2	0	0
elf (5)	0	8	4	0	18	1	0
fpga (36)	0	3	1	60	0	2	114
j120 (28)	442	491	489	448	537	474	572
j30 (17)	0	10	4	0	4	0	2
j60 (18)	56	66	60	56	60	56	62
j90 (17)	0	14	3	0	0	0	1
neos (4)	500	526	523	503	656	500	730
ooo (19)	140	275	343	180	384	258	244
pig-card (20)	2	900	3	903	62	915	903
pig-cl (20)	901	913	948	904	921	939	901
ppp (6)	203	340	336	501	336	500	428
robin (6)	334	505	346	334	517	507	533
13queen (100)	0	5	6	0	24	2	85
11tsp11 (100)	7	18	80	7	428	60	151
vdw (5)	490	695	802	620	825	801	801
Average (669)	260	336	357	352	421	379	412

This table shows the average time spent for solving (in seconds). Time spent for encoding is included.
Timeouts and memory overs are counted as 1000 seconds in the average computation.

Cactus Plot

Enlarged plot from 300 instances to 500 instances

Effect of Reusing/Sharing Counter Matrices

When the reusing/sharing of Counter Matrices is disabled, the performance is declined.

PBSugar: default setting
PBSugar-Noreuse: "-o no_cache,share=0" option is set

Number of instances solved


Family	PBSugar	PBSugar-Noreuse
lopes (200)	81	81
army (12)	8	8
blast (8)	8	7
cache (9)	9	7
chnl (21)	6	6
dbstv30 (5)	5	5
dbstv40 (5)	5	5
dbstv50 (5)	5	5
dlx (3)	3	3
elf (5)	5	5
fpga (36)	36	36
j120 (28)	15	15
j30 (17)	17	17
j60 (18)	17	17
j90 (17)	17	17
neos (4)	2	2
ooo (19)	15	13
pig-card (20)	2	2
pig-cl (20)	2	2
ppp (6)	4	4
robin (6)	3	3
13queen (100)	100	100
11tsp11 (100)	100	100
vdw (5)	2	2
Total (669)	467	462

Time spent for solving


Family	PBSugar	PBSugar-Noreuse
lopes (200)	657	657
army (12)	359	360
blast (8)	83	206
cache (9)	141	276
chnl (21)	761	761
dbstv30 (5)	18	26
dbstv40 (5)	45	60
dbstv50 (5)	107	147
dlx (3)	6	7
elf (5)	8	12
fpga (36)	3	3
j120 (28)	491	491
j30 (17)	10	10
j60 (18)	66	67
j90 (17)	14	14
neos (4)	526	513
ooo (19)	275	342
pig-card (20)	900	900
pig-cl (20)	913	913
ppp (6)	340	340
robin (6)	505	505
13queen (100)	5	5
11tsp11 (100)	18	18
vdw (5)	695	695
Average (669)	336	341

Raw Data

PBSugar: pbsugar-dsl-results.csv
- PB : File name of the PB instance
- FAMILY : Family name of the PB instance
- VARS : Number of PB variables
- PBS : Number of PB constraints
- FIN : Finished (FIN), Timeout (TO), Memory over (MO)
  - Time limit is 1000 seconds
- RESULT : Satisfiable (SAT), Unsatisfiable (UNSAT), Unknown (UNK)
- CPU : Total CPU time in seconds
- ENCODE_CPU : CPU time spent for encoding in seconds
- SAT_CPU : CPU time spent by SAT solver in seconds
- CM : Number of Counter Matrices constructed
- REUSED : Number of times Counter Matrices reused
- SHARED : Number of times Counter Matrices shared
- DECOMP : Number of times PB constraits decomposed
- SAT_VARS : Number of SAT variables
- SAT_CLAUSES : Number of SAT clauses
Other solvers executed on our environment: pbother-dsl-results.csv
- PB : File name of the PB instance
- SOLVER : Solver name
- FIN : Finished (FIN), Timeout (TO), Memory over (MO)
  - Time limit is 1000 seconds
- RESULT : Satisfiable (SAT), Unsatisfiable (UNSAT), Unknown (UNK)
- CPU : Total CPU time in seconds

Table of PBSugar Raw Data


PB	FAMILY	VARS	PBS	FIN	RESULT	CPU	ENCODE_CPU	SAT_CPU	CM	REUSED	SHARED	DECOMP	SAT_VARS	SAT_CLAUSES
normalized-01.opb	lopes	9057	194925	FIN	SAT	145.51	14.66	130.70	703	0	0	0	19698	278033
normalized-02.opb	lopes	7069	151430	FIN	UNSAT	92.31	12.41	79.77	546	0	0	0	15328	215936
normalized-03.opb	lopes	8412	181707	FIN	SAT	48.05	14.29	33.58	655	0	0	0	18321	259182
normalized-04.opb	lopes	6426	138234	FIN	UNSAT	33.22	11.61	21.49	498	0	0	0	13953	197107
normalized-05.opb	lopes	7351	155824	FIN	SAT	258.31	13.13	245.05	563	0	0	0	15883	222262
normalized-06.opb	lopes	3164	67146	FIN	SAT	9.59	8.54	0.98	242	0	0	0	6827	95793
normalized-07.opb	lopes	7175	155089	FIN	SAT	22.06	12.65	9.27	559	0	0	0	15632	221243
normalized-08.opb	lopes	5191	111638	FIN	UNSAT	15.73	10.61	5.02	402	0	0	0	11266	159190
normalized-09.opb	lopes	5398	114743	FIN	UNSAT	24.90	10.29	14.51	415	0	0	0	11686	163753
normalized-100.opb	lopes	10086	226240	TO	UNK	T	13.08	T	720	0	0	0	21738	318834
normalized-101.opb	lopes	7936	176837	FIN	UNSAT	75.43	11.32	63.98	563	0	0	0	17045	249176
normalized-102.opb	lopes	12587	283937	TO	UNK	T	16.24	T	903	0	0	0	27198	400140
normalized-103.opb	lopes	10086	226240	TO	UNK	T	13.09	T	720	0	0	0	21738	318834
normalized-104.opb	lopes	16024	353350	FIN	SAT	44.70	22.18	22.25	1261	0	0	0	34978	502721
normalized-105.opb	lopes	33731	740544	TO	UNK	T	39.58	T	2643	0	0	0	73511	1053242
normalized-106.opb	lopes	39025	858412	TO	UNK	T	46.54	T	3062	0	0	0	85096	1220734
normalized-107.opb	lopes	10238	224043	FIN	SAT	23.91	16.45	7.29	800	0	0	0	22271	318813
normalized-108.opb	lopes	33731	740544	TO	UNK	T	39.79	T	2643	0	0	0	73511	1053242
normalized-1096.cudf.paranoid.opb	lopes	1	1	FIN	SAT	0.16	0.07	0.07	0	0	0	0	1	1
normalized-109.opb	lopes	11274	247096	FIN	SAT	25.03	15.35	9.49	882	0	0	0	24537	351583
normalized-10.opb	lopes	7880	170354	FIN	SAT	39.20	13.51	25.55	614	0	0	0	17168	242998
normalized-110.opb	lopes	39025	858412	TO	UNK	T	46.12	T	3062	0	0	0	85096	1220734
normalized-111.opb	lopes	33692	740354	TO	UNK	T	39.65	T	2642	0	0	0	73451	1052961
normalized-112.opb	lopes	33692	740354	TO	UNK	T	39.67	T	2642	0	0	0	73451	1052961
normalized-113.opb	lopes	8316	181309	FIN	SAT	19.81	14.14	5.52	648	0	0	0	18069	258067
normalized-114.opb	lopes	28939	633938	TO	UNK	T	35.52	T	2264	0	0	0	63028	901752
normalized-115.opb	lopes	16024	353350	FIN	SAT	44.46	23.21	20.97	1261	0	0	0	34978	502721
normalized-116.opb	lopes	44846	988104	TO	UNK	T	52.61	T	3523	0	0	0	97838	1405027
normalized-117.opb	lopes	10238	224043	FIN	SAT	28.75	15.63	12.95	800	0	0	0	22271	318813
normalized-118.opb	lopes	11274	247096	FIN	SAT	27.40	17.53	9.69	882	0	0	0	24537	351583
normalized-119.opb	lopes	48411	1121517	TO	UNK	T	58.71	T	3523	0	0	0	104950	1575406
normalized-11.opb	lopes	5895	126892	FIN	UNSAT	22.04	11.47	10.44	457	0	0	0	12801	180934
normalized-120.opb	lopes	48411	1121517	TO	UNK	T	59.95	T	3523	0	0	0	104950	1575406
normalized-121.opb	lopes	55296	1282690	TO	UNK	T	66.55	T	4030	0	0	0	119978	1801984
normalized-122.opb	lopes	48411	1121517	TO	UNK	T	59.70	T	3523	0	0	0	104950	1575406
normalized-123.opb	lopes	36611	853935	FIN	SAT	532.56	45.95	485.97	2685	0	0	0	79668	1200159
normalized-124.opb	lopes	29741	692942	FIN	UNSAT	575.11	40.40	534.13	2178	0	0	0	64655	973761
normalized-125.opb	lopes	55301	1282592	TO	UNK	T	67.55	T	4032	0	0	0	120039	1802175
normalized-126.opb	lopes	48417	1121431	TO	UNK	T	59.65	T	3525	0	0	0	105012	1575609
normalized-127.opb	lopes	48411	1121517	TO	UNK	T	59.73	T	3523	0	0	0	104950	1575406
normalized-128.opb	lopes	46733	1087391	TO	UNK	T	63.30	T	3417	0	0	0	101534	1527780
normalized-129.opb	lopes	48368	1121286	TO	UNK	T	59.25	T	3522	0	0	0	104884	1575075
normalized-12.opb	lopes	3528	75039	FIN	SAT	10.71	9.16	1.48	271	0	0	0	7632	107095
normalized-130.opb	lopes	41972	972388	TO	UNK	T	50.85	T	3056	0	0	0	91018	1366121
normalized-131.opb	lopes	21928	509638	FIN	UNSAT	153.13	30.46	122.27	1602	0	0	0	47612	716211
normalized-132.opb	lopes	55136	1280712	TO	UNK	T	67.66	T	4024	0	0	0	119708	1799290
normalized-133.opb	lopes	48253	1119563	TO	UNK	T	58.56	T	3517	0	0	0	104682	1572736
normalized-134.opb	lopes	48411	1121517	TO	UNK	T	59.21	T	3523	0	0	0	104950	1575406
normalized-135.opb	lopes	55296	1282690	TO	UNK	T	68.76	T	4030	0	0	0	119978	1801984
normalized-136.opb	lopes	48411	1121517	TO	UNK	T	59.05	T	3523	0	0	0	104950	1575406
normalized-137.opb	lopes	48411	1121517	TO	UNK	T	59.78	T	3523	0	0	0	104950	1575406
normalized-138.opb	lopes	48368	1121286	TO	UNK	T	59.20	T	3522	0	0	0	104884	1575075
normalized-139.opb	lopes	35834	835510	FIN	SAT	312.95	48.46	263.86	2626	0	0	0	77930	1174063
normalized-13.opb	lopes	6737	135818	FIN	SAT	50.27	9.38	40.78	562	0	0	0	14673	196273
normalized-140.opb	lopes	47759	1109809	TO	UNK	T	58.63	T	3487	0	0	0	103694	1559170
normalized-141.opb	lopes	42085	974087	TO	UNK	T	50.55	T	3061	0	0	0	91218	1368436
normalized-142.opb	lopes	48260	1119489	TO	UNK	T	59.56	T	3519	0	0	0	104745	1572951
normalized-143.opb	lopes	41972	972388	TO	UNK	T	51.24	T	3056	0	0	0	91018	1366121
normalized-144.opb	lopes	55296	1282690	TO	UNK	T	68.65	T	4030	0	0	0	119978	1801984
normalized-145.opb	lopes	48411	1121517	TO	UNK	T	59.16	T	3523	0	0	0	104950	1575406
normalized-146.opb	lopes	48417	1121431	TO	UNK	T	59.42	T	3525	0	0	0	105012	1575609
normalized-147.opb	lopes	42127	974306	TO	UNK	T	52.57	T	3062	0	0	0	91283	1368755
normalized-148.opb	lopes	48253	1119563	TO	UNK	T	59.25	T	3517	0	0	0	104682	1572736
normalized-149.opb	lopes	54206	1261615	TO	UNK	T	72.83	T	3965	0	0	0	117813	1772669
normalized-14.opb	lopes	5911	120546	FIN	SAT	13.90	8.51	5.26	498	0	0	0	12931	174193
normalized-150.opb	lopes	47326	1100502	TO	UNK	T	65.70	T	3458	0	0	0	102790	1546151
normalized-151.opb	lopes	42127	974306	TO	UNK	T	51.12	T	3062	0	0	0	91283	1368755
normalized-152.opb	lopes	29741	692942	FIN	SAT	188.93	37.09	151.33	2178	0	0	0	64655	973761
normalized-153.opb	lopes	55296	1282690	TO	UNK	T	69.08	T	4030	0	0	0	119978	1801984
normalized-154.opb	lopes	48411	1121517	TO	UNK	T	59.46	T	3523	0	0	0	104950	1575406
normalized-155.opb	lopes	40423	942446	TO	UNK	T	53.11	T	2962	0	0	0	87909	1324285
normalized-156.opb	lopes	38303	893113	FIN	SAT	478.89	51.29	426.93	2807	0	0	0	83302	1254986
normalized-157.opb	lopes	41972	972388	TO	UNK	T	51.22	T	3056	0	0	0	91018	1366121
normalized-158.opb	lopes	113212	2516734	TO	UNK	T	137.51	T	8957	0	0	0	247750	3577421
normalized-159.opb	lopes	102449	2274228	TO	UNK	T	124.76	T	8094	0	0	0	224048	3232622
normalized-15.opb	lopes	6809	146226	FIN	SAT	20.63	12.66	7.85	527	0	0	0	14777	208508
normalized-160.opb	lopes	113386	2518744	TO	UNK	T	140.20	T	8963	0	0	0	248026	3580087
normalized-161.opb	lopes	134842	3153398	TO	UNK	T	174.59	T	9886	0	0	0	293238	4427911
normalized-162.opb	lopes	26339	612374	FIN	SAT	101.71	32.55	68.69	1922	0	0	0	57129	860285
normalized-163.opb	lopes	135027	3155676	TO	UNK	T	174.75	T	9892	0	0	0	293533	4430905
normalized-164.opb	lopes	26339	612374	FIN	SAT	122.30	35.88	85.96	1922	0	0	0	57129	860285
normalized-165.opb	lopes	147764	3459649	TO	UNK	T	202.08	T	10847	0	0	0	321529	4858160
normalized-166.opb	lopes	26339	612374	FIN	SAT	102.18	35.80	65.93	1922	0	0	0	57129	860285
normalized-167.opb	lopes	106196	2493137	TO	UNK	T	148.51	T	7823	0	0	0	231465	3502016
normalized-168.opb	lopes	128666	3016254	TO	UNK	T	180.26	T	9462	0	0	0	280222	4236303
normalized-169.opb	lopes	148486	3472197	TO	UNK	T	191.58	T	10883	0	0	0	322855	4875236
normalized-16.opb	lopes	11658	250186	FIN	SAT	856.60	15.20	841.20	903	0	0	0	25344	356909
normalized-170.opb	lopes	26339	612374	FIN	SAT	110.40	36.94	73.00	1922	0	0	0	57129	860285
normalized-171.opb	lopes	122407	2858957	TO	UNK	T	157.03	T	8963	0	0	0	266042	4014374
normalized-172.opb	lopes	288080	6434441	TO	UNK	T	431.56	T	22886	0	0	0	631607	9145467
normalized-173.opb	lopes	268241	5985144	TO	UNK	T	351.55	T	21283	0	0	0	587741	8506132
normalized-174.opb	lopes	248659	5546518	TO	UNK	T	326.86	T	19724	0	0	0	544768	7882792
normalized-175.opb	lopes	248659	5546518	TO	UNK	T	325.19	T	19724	0	0	0	544768	7882792
normalized-176.opb	lopes	310571	7294179	TO	UNK	T	472.29	T	22857	0	0	0	676552	10241748
normalized-177.opb	lopes	60536	1417665	FIN	SAT	792.58	81.95	709.59	4447	0	0	0	131733	1991272
normalized-178.opb	lopes	334369	7853489	TO	UNK	T	509.70	T	24607	0	0	0	728364	11026750
normalized-179.opb	lopes	311827	7317246	TO	UNK	T	443.32	T	22922	0	0	0	678883	10273055
normalized-17.opb	lopes	9342	199352	TO	UNK	T	12.32	T	720	0	0	0	20256	284392
normalized-180.opb	lopes	311827	7317246	TO	UNK	T	429.19	T	22922	0	0	0	678883	10273055
normalized-181.opb	lopes	335161	7866877	TO	UNK	T	465.69	T	24643	0	0	0	729760	11044666
normalized-182.opb	lopes	599527	14097016	TO	UNK	T	875.45	T	44152	0	0	0	1306333	19791205
normalized-183.opb	lopes	599527	14097016	TO	UNK	T	890.69	T	44152	0	0	0	1306333	19791205
normalized-184.opb	lopes	1025127	24132986	TO	UNK	T	T	T	T	T	T	T	T	T
normalized-185.opb	lopes	1840	46243	FIN	SAT	25.26	6.68	18.54	73	0	0	0	3949	62686
normalized-186.opb	lopes	1103	24920	FIN	UNSAT	118.42	6.46	111.93	42	0	0	0	2370	34392
normalized-187.opb	lopes	1508	33299	FIN	SAT	4.93	4.29	0.61	73	0	0	0	3257	46610
normalized-188.opb	lopes	483	8027	FIN	UNSAT	2.77	2.38	0.37	21	0	0	0	1038	11851
normalized-189.opb	lopes	14685	417306	TO	UNK	T	20.40	T	730	0	0	0	31195	557479
normalized-18.opb	lopes	9342	199352	FIN	SAT	122.68	12.59	109.90	720	0	0	0	20256	284392
normalized-190.opb	lopes	11586	326275	TO	UNK	T	16.23	T	573	0	0	0	24587	436275
normalized-191.opb	lopes	22941	594926	TO	UNK	T	29.78	T	1359	0	0	0	49143	812886
normalized-192.opb	lopes	15414	395824	TO	UNK	T	20.37	T	907	0	0	0	32942	541207
normalized-193.opb	lopes	12360	315408	TO	UNK	T	16.46	T	724	0	0	0	26368	431404
normalized-19.opb	lopes	7351	155824	FIN	UNSAT	512.38	10.38	501.88	563	0	0	0	15883	222262
normalized-20.opb	lopes	9342	199352	FIN	SAT	317.28	12.46	304.66	720	0	0	0	20256	284392
normalized-21.opb	lopes	7351	155824	FIN	UNSAT	354.10	13.43	340.55	563	0	0	0	15883	222262
normalized-22.opb	lopes	9355	199372	TO	UNK	T	12.38	T	722	0	0	0	20320	284674
normalized-22s.smv.opb	lopes	5985	15365	FIN	UNSAT	13.85	9.11	4.73	632	720	0	0	326409	1446845
normalized-23.opb	lopes	7365	155855	TO	UNK	T	10.47	T	565	0	0	0	15948	222555
normalized-24.opb	lopes	9342	199352	TO	UNK	T	12.18	T	720	0	0	0	20256	284392
normalized-25.opb	lopes	7351	155824	FIN	UNSAT	184.21	10.36	173.72	563	0	0	0	15883	222262
normalized-25s.smv.opb	lopes	5072	12829	FIN	UNSAT	11.93	8.29	3.61	514	594	0	0	265670	1177039
normalized-26.opb	lopes	7351	155824	FIN	SAT	193.13	9.96	183.05	563	0	0	0	15883	222262
normalized-27.opb	lopes	9355	199372	TO	UNK	T	12.88	T	722	0	0	0	20320	284674
normalized-28.opb	lopes	7365	155855	TO	UNK	T	10.14	T	565	0	0	0	15948	222555
normalized-29.opb	lopes	9220	197914	FIN	SAT	294.69	12.94	281.58	714	0	0	0	20032	282298
normalized-30.opb	lopes	7231	154408	FIN	UNSAT	55.74	9.82	45.79	557	0	0	0	15661	220190
normalized-31.opb	lopes	9310	199239	FIN	SAT	404.65	12.02	392.47	719	0	0	0	20203	284188
normalized-32.opb	lopes	7320	155722	FIN	UNSAT	210.87	10.25	200.49	562	0	0	0	15831	222069
normalized-33.opb	lopes	7085	151483	FIN	SAT	112.65	11.39	101.11	548	0	0	0	15395	216251
normalized-34.opb	lopes	5398	114743	FIN	UNSAT	34.54	11.33	23.09	415	0	0	0	11686	163753
normalized-35.opb	lopes	9220	197914	FIN	SAT	109.15	11.97	97.03	714	0	0	0	20032	282298
normalized-36.opb	lopes	7231	154408	FIN	UNSAT	84.93	10.75	74.06	557	0	0	0	15661	220190
normalized-37.opb	lopes	9310	199239	FIN	SAT	556.40	12.30	543.95	719	0	0	0	20203	284188
normalized-37s.smv.opb	lopes	1190	3183	FIN	UNSAT	3.01	2.80	0.19	24	104	0	0	4142	16167
normalized-38.opb	lopes	7320	155722	FIN	UNSAT	51.62	10.19	41.29	562	0	0	0	15831	222069
normalized-39.opb	lopes	11658	250186	TO	UNK	T	15.11	T	903	0	0	0	25344	356909
normalized-40.opb	lopes	9342	199352	TO	UNK	T	11.71	T	720	0	0	0	20256	284392
normalized-41.opb	lopes	5690	119124	FIN	SAT	84.61	8.58	75.93	434	0	0	0	12302	170328
normalized-42.opb	lopes	4276	88544	FIN	UNSAT	33.43	6.93	26.42	323	0	0	0	9196	126597
normalized-43.opb	lopes	7175	155089	FIN	SAT	22.22	12.83	9.23	559	0	0	0	15632	221243
normalized-43s.smv.opb	lopes	3655	8686	FIN	UNSAT	9.29	6.35	2.92	324	380	0	0	167893	742414
normalized-44.opb	lopes	5191	111638	FIN	UNSAT	16.89	10.45	6.35	402	0	0	0	11266	159190
normalized-44s.smv.opb	lopes	495	940	FIN	UNSAT	4.60	4.33	0.25	64	76	0	0	16545	72240
normalized-45.opb	lopes	4289	91910	FIN	SAT	10.96	9.57	1.31	331	0	0	0	9293	131076
normalized-46.opb	lopes	12552	283802	TO	UNK	T	15.44	T	902	0	0	0	27140	399905
normalized-46s.smv.opb	lopes	1612	3653	FIN	UNSAT	6.24	5.61	0.61	166	214	0	0	43278	188743
normalized-47.opb	lopes	10052	226117	TO	UNK	T	13.31	T	719	0	0	0	21681	318611
normalized-48.opb	lopes	9956	224622	FIN	SAT	352.57	13.16	339.23	714	0	0	0	21498	316500
normalized-49.opb	lopes	7808	175243	FIN	UNSAT	72.37	11.40	60.83	557	0	0	0	16807	246866
normalized-50.opb	lopes	10086	226240	TO	UNK	T	13.66	T	720	0	0	0	21738	318834
normalized-51.opb	lopes	7936	176837	FIN	UNSAT	55.68	11.74	43.79	563	0	0	0	17045	249176
normalized-52.opb	lopes	12587	283937	TO	UNK	T	15.89	T	903	0	0	0	27198	400140
normalized-53.opb	lopes	10086	226240	TO	UNK	T	13.99	T	720	0	0	0	21738	318834
normalized-54.opb	lopes	10086	226240	FIN	SAT	597.57	13.62	583.79	720	0	0	0	21738	318834
normalized-55.opb	lopes	7936	176837	FIN	UNSAT	183.82	10.75	172.93	563	0	0	0	17045	249176
normalized-56.opb	lopes	15466	350566	TO	UNK	T	19.21	T	1114	0	0	0	33484	493990
normalized-57.opb	lopes	12587	283937	TO	UNK	T	16.52	T	903	0	0	0	27198	400140
normalized-58.opb	lopes	12587	283937	TO	UNK	T	16.33	T	903	0	0	0	27198	400140
normalized-59.opb	lopes	10086	226240	TO	UNK	T	12.79	T	720	0	0	0	21738	318834
normalized-60.opb	lopes	12587	283937	TO	UNK	T	17.18	T	903	0	0	0	27198	400140
normalized-61.opb	lopes	10086	226240	TO	UNK	T	13.40	T	720	0	0	0	21738	318834
normalized-62.opb	lopes	12587	283937	TO	UNK	T	16.83	T	903	0	0	0	27198	400140
normalized-63.opb	lopes	10086	226240	TO	UNK	T	13.83	T	720	0	0	0	21738	318834
normalized-64.opb	lopes	12587	283937	TO	UNK	T	16.45	T	903	0	0	0	27198	400140
normalized-65.opb	lopes	10086	226240	TO	UNK	T	13.24	T	720	0	0	0	21738	318834
normalized-66.opb	lopes	12587	283937	TO	UNK	T	16.52	T	903	0	0	0	27198	400140
normalized-67.opb	lopes	10086	226240	TO	UNK	T	13.65	T	720	0	0	0	21738	318834
normalized-68.opb	lopes	12552	283802	TO	UNK	T	15.56	T	902	0	0	0	27140	399905
normalized-69.opb	lopes	10052	226117	TO	UNK	T	12.87	T	719	0	0	0	21681	318611
normalized-70.opb	lopes	12552	283802	TO	UNK	T	15.53	T	902	0	0	0	27140	399905
normalized-71.opb	lopes	10052	226117	TO	UNK	T	13.34	T	719	0	0	0	21681	318611
normalized-72.opb	lopes	10086	226240	TO	UNK	T	13.42	T	720	0	0	0	21738	318834
normalized-73.opb	lopes	7936	176837	FIN	UNSAT	415.64	11.71	403.79	563	0	0	0	17045	249176
normalized-74.opb	lopes	12587	283937	TO	UNK	T	15.92	T	903	0	0	0	27198	400140
normalized-75.opb	lopes	10086	226240	TO	UNK	T	13.76	T	720	0	0	0	21738	318834
normalized-76.opb	lopes	12587	283937	TO	UNK	T	16.26	T	903	0	0	0	27198	400140
normalized-77.opb	lopes	10086	226240	TO	UNK	T	13.44	T	720	0	0	0	21738	318834
normalized-78.opb	lopes	15430	350419	TO	UNK	T	19.34	T	1113	0	0	0	33425	493743
normalized-79.opb	lopes	12552	283802	TO	UNK	T	16.73	T	902	0	0	0	27140	399905
normalized-80.opb	lopes	12587	283937	TO	UNK	T	16.55	T	903	0	0	0	27198	400140
normalized-81.opb	lopes	10086	226240	TO	UNK	T	13.23	T	720	0	0	0	21738	318834
normalized-82.opb	lopes	12455	282295	TO	UNK	T	16.11	T	897	0	0	0	26956	397782
normalized-83.opb	lopes	9956	224622	TO	UNK	T	13.44	T	714	0	0	0	21498	316500
normalized-84.opb	lopes	6426	138234	FIN	UNSAT	25.95	11.51	14.33	498	0	0	0	13953	197107
normalized-85.opb	lopes	9500	215324	FIN	SAT	151.06	15.38	135.46	684	0	0	0	20548	303390
normalized-86.opb	lopes	7354	165969	FIN	UNSAT	33.11	13.05	19.92	527	0	0	0	15859	233780
normalized-87.opb	lopes	6368	144031	FIN	UNSAT	18.97	12.10	6.75	457	0	0	0	13739	202870
normalized-88.opb	lopes	12587	283937	TO	UNK	T	16.77	T	903	0	0	0	27198	400140
normalized-89.opb	lopes	10086	226240	TO	UNK	T	13.84	T	720	0	0	0	21738	318834
normalized-90.opb	lopes	12587	283937	TO	UNK	T	15.88	T	903	0	0	0	27198	400140
normalized-91.opb	lopes	10086	226240	TO	UNK	T	13.64	T	720	0	0	0	21738	318834
normalized-92.opb	lopes	9086	206245	FIN	SAT	283.57	15.47	267.95	655	0	0	0	19663	290599
normalized-93.opb	lopes	6941	156902	FIN	UNSAT	44.14	12.48	31.55	498	0	0	0	14975	221001
normalized-94.opb	lopes	12587	283937	TO	UNK	T	16.94	T	903	0	0	0	27198	400140
normalized-95.opb	lopes	10086	226240	TO	UNK	T	13.31	T	720	0	0	0	21738	318834
normalized-96.opb	lopes	12587	283937	TO	UNK	T	16.70	T	903	0	0	0	27198	400140
normalized-97.opb	lopes	10086	226240	TO	UNK	T	13.27	T	720	0	0	0	21738	318834
normalized-98.opb	lopes	10052	226117	FIN	SAT	778.24	12.38	765.68	719	0	0	0	21681	318611
normalized-99.opb	lopes	7903	176726	FIN	UNSAT	46.61	10.87	35.60	562	0	0	0	16989	248965
normalized-army10.14bt.opb	army	316	686	FIN	SAT	24.62	2.80	21.80	9	1	0	1	4315	20502
normalized-army10.14ls.opb	army	316	476	FIN	SAT	4.63	2.00	2.61	2	0	0	0	3106	14766
normalized-army11.17bt.opb	army	370	809	TO	UNK	T	3.06	T	9	1	0	1	5629	26997
normalized-army11.17ls.opb	army	370	557	FIN	SAT	14.07	2.24	11.81	2	0	0	0	4420	21219
normalized-army12.21bt.opb	army	428	942	TO	UNK	T	2.83	T	9	1	0	1	8762	42144
normalized-army12.21ls.opb	army	428	644	TO	UNK	T	2.76	T	2	0	0	0	6302	30502
normalized-army13.24bt.opb	army	490	1085	TO	UNK	T	3.51	T	9	1	0	1	10800	52255
normalized-army13.24ls.opb	army	490	737	FIN	SAT	243.46	3.03	240.41	2	0	0	0	8340	40563
normalized-army8.9bt.opb	army	220	470	FIN	SAT	2.06	1.89	0.15	9	1	0	1	1992	9256
normalized-army8.9ls.opb	army	220	332	FIN	SAT	2.84	1.45	1.37	2	0	0	0	1410	6498
normalized-army9.12bt.opb	army	266	573	FIN	SAT	3.27	2.43	0.81	9	1	0	1	2798	13215
normalized-army9.12ls.opb	army	266	401	FIN	SAT	12.51	1.68	10.81	2	0	0	0	2216	10423
normalized-blast-floppy1-2.ucl.opb	blast	152	127	FIN	UNSAT	4.60	4.15	0.43	26	24	0	0	39206	175417
normalized-blast-floppy1-3.ucl.opb	blast	274	259	FIN	UNSAT	3.87	3.73	0.12	47	53	0	0	11099	48326
normalized-blast-floppy1-4.ucl.opb	blast	237	197	FIN	UNSAT	3.46	3.28	0.16	38	36	0	0	32763	146011
normalized-blast-floppy1-6.ucl.opb	blast	719	593	FIN	UNSAT	8.84	6.96	1.86	107	115	0	0	190830	854096
normalized-blast-floppy1-7.ucl.opb	blast	2913	3105	FIN	UNSAT	219.35	212.30	7.03	411	435	0	0	5836444	26244010
normalized-blast-floppy1-8.ucl.opb	blast	3618	3931	FIN	UNSAT	304.91	295.60	9.29	521	545	0	0	7998465	35967700
normalized-blast-tlan2.ucl.opb	blast	2221	3050	FIN	UNSAT	18.22	14.72	3.48	357	363	0	0	726414	3254775
normalized-blast-tlan3.ucl.opb	blast	19944	50842	FIN	UNSAT	97.56	93.28	4.22	3470	3474	0	0	7099932	31839856
normalized-cache-ibm-q-full.all.ucl.opb	cache	81558	240469	FIN	UNSAT	363.78	17.96	345.61	2128	2476	0	0	615386	2611941
normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb	cache	87751	254772	FIN	UNSAT	51.09	32.15	18.75	3247	4465	0	0	1500818	6562585
normalized-cache-ibm-q-unbounded.Icl2arity.ucl.opb	cache	23837	67568	FIN	UNSAT	16.66	10.60	6.00	1335	1835	0	0	311512	1343807
normalized-cache-ibm-q-unbounded.Ih1arity.ucl.opb	cache	201731	592525	FIN	UNSAT	662.82	60.62	601.78	5258	7838	0	0	2542615	11043059
normalized-cache-ibm-q-unbounded.Ih2arity.ucl.opb	cache	76091	218262	FIN	SAT	42.71	37.08	5.42	4451	6201	0	0	2006748	8836439
normalized-cache.inv10.ucl.opb	cache	8937	26319	FIN	UNSAT	5.50	4.86	0.60	136	136	0	0	16961	60999
normalized-cache.inv12.ucl.opb	cache	25800	76699	FIN	UNSAT	8.79	7.32	1.41	190	190	0	0	37010	125149
normalized-cache.inv14.ucl.opb	cache	62704	187107	FIN	UNSAT	132.13	12.29	119.70	252	252	0	0	93700	323439
normalized-cache.inv8.ucl.opb	cache	2355	6744	FIN	UNSAT	4.70	4.46	0.22	88	88	0	0	7547	29184
normalized-chnl10_11_pb.cnf.cr.opb	chnl	220	42	FIN	UNSAT	1.00	0.67	0.31	20	0	0	0	640	1842
normalized-chnl10_15_pb.cnf.cr.opb	chnl	300	50	FIN	UNSAT	1.12	0.54	0.55	20	0	0	0	880	2570
normalized-chnl10_20_pb.cnf.cr.opb	chnl	400	60	FIN	UNSAT	1.42	0.77	0.63	20	0	0	0	1180	3480
normalized-chnl15_16_pb.cnf.cr.opb	chnl	480	62	FIN	UNSAT	393.35	1.63	391.69	30	0	0	0	1410	4112
normalized-chnl15_20_pb.cnf.cr.opb	chnl	600	70	FIN	UNSAT	328.11	0.89	327.19	30	0	0	0	1770	5200
normalized-chnl15_25_pb.cnf.cr.opb	chnl	750	80	FIN	UNSAT	267.75	2.36	265.37	30	0	0	0	2220	6560
normalized-chnl20_21_pb.cnf.cr.opb	chnl	840	82	TO	UNK	T	2.60	T	40	0	0	0	2480	7282
normalized-chnl20_25_pb.cnf.cr.opb	chnl	1000	90	TO	UNK	T	2.66	T	40	0	0	0	2960	8730
normalized-chnl20_30_pb.cnf.cr.opb	chnl	1200	100	TO	UNK	T	2.90	T	40	0	0	0	3560	10540
normalized-chnl30_31_pb.cnf.cr.opb	chnl	1860	122	TO	UNK	T	3.44	T	60	0	0	0	5520	16322
normalized-chnl30_35_pb.cnf.cr.opb	chnl	2100	130	TO	UNK	T	3.08	T	60	0	0	0	6240	18490
normalized-chnl30_40_pb.cnf.cr.opb	chnl	2400	140	TO	UNK	T	2.88	T	60	0	0	0	7140	21200
normalized-chnl35_36_pb.cnf.cr.opb	chnl	2520	142	TO	UNK	T	1.68	T	70	0	0	0	7490	22192
normalized-chnl35_40_pb.cnf.cr.opb	chnl	2800	150	TO	UNK	T	4.26	T	70	0	0	0	8330	24720
normalized-chnl35_45_pb.cnf.cr.opb	chnl	3150	160	TO	UNK	T	2.82	T	70	0	0	0	9380	27880
normalized-chnl40_41_pb.cnf.cr.opb	chnl	3280	162	TO	UNK	T	2.00	T	80	0	0	0	9760	28962
normalized-chnl40_45_pb.cnf.cr.opb	chnl	3600	170	TO	UNK	T	4.60	T	80	0	0	0	10720	31850
normalized-chnl40_50_pb.cnf.cr.opb	chnl	4000	180	TO	UNK	T	2.73	T	80	0	0	0	11920	35460
normalized-chnl50_51_pb.cnf.cr.opb	chnl	5100	202	TO	UNK	T	3.32	T	100	0	0	0	15200	45202
normalized-chnl50_55_pb.cnf.cr.opb	chnl	5500	210	TO	UNK	T	3.60	T	100	0	0	0	16400	48810
normalized-chnl50_60_pb.cnf.cr.opb	chnl	6000	220	TO	UNK	T	3.45	T	100	0	0	0	17900	53320
normalized-dbst_v30_e350_d15_mw10_1.opb.PB06.opb	dbstv30	1600	328901	FIN	SAT	17.71	15.97	1.46	121	1710	0	0	41675	523357
normalized-dbst_v30_e350_d15_mw10_2.opb.PB06.opb	dbstv30	1600	328901	FIN	SAT	17.48	15.77	1.48	121	1710	0	0	41555	522757
normalized-dbst_v30_e350_d15_mw10_3.opb.PB06.opb	dbstv30	1600	328901	FIN	SAT	18.01	16.31	1.47	121	1710	0	0	41334	521652
normalized-dbst_v30_e350_d15_mw10_8.opb.PB06.opb	dbstv30	1600	328901	FIN	SAT	17.70	16.02	1.46	121	1710	0	0	42157	525767
normalized-dbst_v30_e350_d15_mw10_9.opb.PB06.opb	dbstv30	1600	328901	FIN	SAT	16.46	14.68	1.56	121	1710	0	0	41253	521247
normalized-dbst_v40_e600_d20_mw10_0.opb.PB06.opb	dbstv40	2800	990001	FIN	SAT	43.83	39.42	3.74	161	3080	0	0	94768	1439682
normalized-dbst_v40_e600_d20_mw10_2.opb.PB06.opb	dbstv40	2800	990001	FIN	SAT	44.79	40.26	3.89	161	3080	0	0	92805	1429867
normalized-dbst_v40_e600_d20_mw10_5.opb.PB06.opb	dbstv40	2800	990001	FIN	SAT	44.11	39.57	3.88	161	3080	0	0	93708	1434382
normalized-dbst_v40_e600_d20_mw10_6.opb.PB06.opb	dbstv40	2800	990001	FIN	SAT	44.11	39.60	3.85	161	3080	0	0	93306	1432372
normalized-dbst_v40_e600_d20_mw10_9.opb.PB06.opb	dbstv40	2800	990001	FIN	SAT	41.84	37.34	3.87	161	3080	0	0	94311	1437397
normalized-dbst_v50_e1000_d25_mw10_1.opb.PB06.opb	dbstv50	4500	2559501	FIN	SAT	107.73	96.76	9.35	201	4850	0	0	192958	3485592
normalized-dbst_v50_e1000_d25_mw10_3.opb.PB06.opb	dbstv50	4500	2559501	FIN	SAT	106.27	95.02	9.45	201	4850	0	0	192222	3481912
normalized-dbst_v50_e1000_d25_mw10_5.opb.PB06.opb	dbstv50	4500	2559501	FIN	SAT	103.16	92.11	9.41	201	4850	0	0	191005	3475827
normalized-dbst_v50_e1000_d25_mw10_6.opb.PB06.opb	dbstv50	4500	2559501	FIN	SAT	104.68	93.52	9.59	201	4850	0	0	191419	3477897
normalized-dbst_v50_e1000_d25_mw10_9.opb.PB06.opb	dbstv50	4500	2559501	FIN	SAT	105.71	94.82	9.31	201	4850	0	0	191911	3480357
normalized-dlx1c.rwmem1.ucl.opb	dlx	7578	21401	FIN	UNSAT	5.15	3.97	1.15	386	514	0	0	50448	209635
normalized-dlx1c.rwmem.ucl.opb	dlx	9051	25833	FIN	UNSAT	5.47	4.20	1.23	382	510	0	0	51685	213047
normalized-dlx1c.ucl.opb	dlx	6392	18058	FIN	UNSAT	4.74	3.75	0.96	326	454	0	0	45466	189848
normalized-elf.rf10.ucl.opb	elf	55066	160619	FIN	UNSAT	19.14	13.10	5.89	1361	2671	0	0	381051	1608234
normalized-elf.rf6.ucl.opb	elf	67	132	FIN	UNSAT	0.36	0.26	0.08	4	8	0	0	175	584
normalized-elf.rf7.ucl.opb	elf	1328	3349	FIN	UNSAT	4.76	4.53	0.21	66	118	0	0	7910	32191
normalized-elf.rf8.ucl.opb	elf	6059	16684	FIN	UNSAT	6.08	5.26	0.80	286	458	0	0	40565	168414
normalized-elf.rf9.ucl.opb	elf	20445	58444	FIN	UNSAT	9.21	6.58	2.58	696	1328	0	0	169033	717452
normalized-fpga10_10_sat_pb.cnf.cr.opb	fpga	150	130	FIN	SAT	0.79	0.67	0.11	20	0	0	0	430	1300
normalized-fpga10_8_sat_pb.cnf.cr.opb	fpga	120	106	FIN	SAT	0.43	0.32	0.09	18	0	0	0	342	1024
normalized-fpga10_9_sat_pb.cnf.cr.opb	fpga	135	118	FIN	SAT	0.63	0.54	0.07	19	0	0	0	386	1162
normalized-fpga11_10_sat_pb.cnf.cr.opb	fpga	165	141	FIN	SAT	1.02	0.89	0.11	21	0	0	0	474	1437
normalized-fpga11_11_sat_pb.cnf.cr.opb	fpga	182	154	FIN	SAT	1.04	0.90	0.12	22	0	0	0	524	1594
normalized-fpga11_9_sat_pb.cnf.cr.opb	fpga	149	128	FIN	SAT	0.51	0.38	0.11	20	0	0	0	427	1289
normalized-fpga12_10_sat_pb.cnf.cr.opb	fpga	180	152	FIN	SAT	1.21	1.08	0.11	22	0	0	0	518	1574
normalized-fpga12_11_sat_pb.cnf.cr.opb	fpga	198	166	FIN	SAT	1.26	1.11	0.13	23	0	0	0	571	1741
normalized-fpga12_12_sat_pb.cnf.cr.opb	fpga	216	180	FIN	SAT	1.44	1.17	0.25	24	0	0	0	624	1908
normalized-fpga13_11_sat_pb.cnf.cr.opb	fpga	215	178	FIN	SAT	1.25	1.12	0.11	24	0	0	0	621	1897
normalized-fpga13_12_sat_pb.cnf.cr.opb	fpga	234	193	FIN	SAT	1.50	1.37	0.11	25	0	0	0	677	2074
normalized-fpga13_13_sat_pb.cnf.cr.opb	fpga	254	208	FIN	SAT	1.60	1.46	0.12	26	0	0	0	736	2260
normalized-fpga14_12_sat_pb.cnf.cr.opb	fpga	252	206	FIN	SAT	1.50	1.37	0.11	26	0	0	0	730	2240
normalized-fpga14_13_sat_pb.cnf.cr.opb	fpga	273	222	FIN	SAT	1.63	1.46	0.14	27	0	0	0	792	2436
normalized-fpga14_14_sat_pb.cnf.cr.opb	fpga	294	238	FIN	SAT	0.95	0.80	0.13	28	0	0	0	854	2632
normalized-fpga15_13_sat_pb.cnf.cr.opb	fpga	293	236	FIN	SAT	1.87	1.72	0.12	28	0	0	0	851	2621
normalized-fpga15_14_sat_pb.cnf.cr.opb	fpga	315	253	FIN	SAT	1.94	1.77	0.15	29	0	0	0	916	2827
normalized-fpga15_15_sat_pb.cnf.cr.opb	fpga	338	270	FIN	SAT	2.24	2.07	0.15	30	0	0	0	984	3042
normalized-fpga20_18_sat_pb.cnf.cr.opb	fpga	540	416	FIN	SAT	3.07	2.82	0.23	38	0	0	0	1582	4934
normalized-fpga20_19_sat_pb.cnf.cr.opb	fpga	570	438	FIN	SAT	3.25	3.07	0.16	39	0	0	0	1671	5217
normalized-fpga20_20_sat_pb.cnf.cr.opb	fpga	600	460	FIN	SAT	3.38	3.04	0.32	40	0	0	0	1760	5500
normalized-fpga25_23_sat_pb.cnf.cr.opb	fpga	863	646	FIN	SAT	3.96	3.73	0.20	48	0	0	0	2541	7981
normalized-fpga25_24_sat_pb.cnf.cr.opb	fpga	900	673	FIN	SAT	4.05	3.79	0.24	49	0	0	0	2651	8332
normalized-fpga25_25_sat_pb.cnf.cr.opb	fpga	938	700	FIN	SAT	4.33	4.06	0.25	50	0	0	0	2764	8692
normalized-fpga30_28_sat_pb.cnf.cr.opb	fpga	1260	926	FIN	SAT	4.40	4.10	0.28	58	0	0	0	3722	11744
normalized-fpga30_29_sat_pb.cnf.cr.opb	fpga	1305	958	FIN	SAT	5.02	4.30	0.70	59	0	0	0	3856	12172
normalized-fpga30_30_sat_pb.cnf.cr.opb	fpga	1350	990	FIN	SAT	5.12	4.70	0.40	60	0	0	0	3990	12600
normalized-fpga35_33_sat_pb.cnf.cr.opb	fpga	1733	1256	FIN	SAT	3.62	3.17	0.43	68	0	0	0	5131	16241
normalized-fpga35_34_sat_pb.cnf.cr.opb	fpga	1785	1293	FIN	SAT	7.19	5.00	2.17	69	0	0	0	5286	16737
normalized-fpga35_35_sat_pb.cnf.cr.opb	fpga	1838	1330	FIN	SAT	13.08	5.01	8.05	70	0	0	0	5444	17242
normalized-fpga40_38_sat_pb.cnf.cr.opb	fpga	2280	1636	FIN	SAT	3.52	3.13	0.37	78	0	0	0	6762	21454
normalized-fpga40_39_sat_pb.cnf.cr.opb	fpga	2340	1678	FIN	SAT	5.50	5.10	0.38	79	0	0	0	6941	22027
normalized-fpga40_40_sat_pb.cnf.cr.opb	fpga	2400	1720	FIN	SAT	5.58	5.14	0.42	80	0	0	0	7120	22600
normalized-fpga45_43_sat_pb.cnf.cr.opb	fpga	2903	2066	FIN	SAT	4.27	3.78	0.47	88	0	0	0	8621	27401
normalized-fpga45_44_sat_pb.cnf.cr.opb	fpga	2970	2113	FIN	SAT	6.41	3.78	2.61	89	0	0	0	8821	28042
normalized-fpga45_45_sat_pb.cnf.cr.opb	fpga	3038	2160	FIN	SAT	4.93	3.88	1.02	90	0	0	0	9024	28692
normalized-j12010_10-sat.opb	j120	16214	50734	FIN	SAT	16.27	10.00	6.22	264	0	0	0	592922	2892364
normalized-j12013_1-unsat.opb	j120	29282	92908	FIN	UNSAT	16.45	15.19	1.18	480	0	0	0	942482	4586668
normalized-j12015_3-unsat.opb	j120	21054	66352	FIN	UNSAT	15.42	14.22	1.12	344	0	0	0	1034908	5074734
normalized-j1201_5-sat.opb	j120	27346	86712	FIN	SAT	9.68	6.81	2.81	448	0	0	0	138002	614008
normalized-j12016_4-sat.opb	j120	48642	155800	TO	UNK	T	23.50	T	800	0	0	0	1458442	7074000
normalized-j12021_4-sat.opb	j120	32912	109489	FIN	SAT	14.62	9.64	4.89	540	0	0	0	158732	706999
normalized-j12022_9-sat.opb	j120	26620	88108	FIN	SAT	11.01	8.39	2.54	436	0	0	0	154259	698617
normalized-j12023_3-unsat.opb	j120	23958	79333	FIN	UNSAT	9.13	8.46	0.61	392	0	0	0	166842	767685
normalized-j12026_5-unsat.opb	j120	32912	109848	FIN	UNSAT	405.30	11.21	393.99	540	0	0	0	340037	1595388
normalized-j12027_7-unsat.opb	j120	27588	91561	FIN	UNSAT	29.58	10.72	18.76	452	0	0	0	376306	1790064
normalized-j12032_3-unsat.opb	j120	32186	107047	TO	UNK	T	14.72	T	528	0	0	0	821018	3977815
normalized-j12032_8-unsat.opb	j120	31460	104814	TO	UNK	T	14.66	T	516	0	0	0	794753	3849555
normalized-j1203_2-sat.opb	j120	21538	67936	FIN	SAT	9.90	7.59	2.25	352	0	0	0	149930	686488
normalized-j12033_3-sat.opb	j120	26136	86824	TO	UNK	T	14.15	T	428	0	0	0	854530	4163738
normalized-j12034_4-sat.opb	j120	23232	76633	FIN	SAT	42.19	14.82	27.31	380	0	0	0	1118677	5487548
normalized-j12036_3-sat.opb	j120	55660	186884	TO	UNK	T	25.00	T	916	0	0	0	1480956	7167262
normalized-j12036_4-sat.opb	j120	57354	192702	TO	UNK	T	25.77	T	944	0	0	0	1408926	6800466
normalized-j12037_7-sat.opb	j120	39204	130975	TO	UNK	T	21.46	T	644	0	0	0	1412212	6884603
normalized-j12038_8-unsat.opb	j120	29040	96434	TO	UNK	T	17.35	T	476	0	0	0	1483815	7279393
normalized-j12041_4-unsat.opb	j120	28072	97590	FIN	UNSAT	11.69	8.83	2.79	460	0	0	0	130537	584385
normalized-j12045_10-sat.opb	j120	24200	83750	FIN	SAT	11.72	8.85	2.81	396	0	0	0	185075	858821
normalized-j12047_10-unsat.opb	j120	30492	105829	TO	UNK	T	11.76	T	500	0	0	0	437742	2090954
normalized-j1205_1-unsat.opb	j120	22264	70239	FIN	UNSAT	9.04	8.34	0.64	364	0	0	0	198076	920543
normalized-j12052_5-unsat.opb	j120	37752	131628	TO	UNK	T	16.10	T	620	0	0	0	801282	3867748
normalized-j12056_10-unsat.opb	j120	57354	201250	TO	UNK	T	25.43	T	944	0	0	0	1303906	6288162
normalized-j12058_4-sat.opb	j120	35332	122962	TO	UNK	T	21.38	T	580	0	0	0	1542027	7552037
normalized-j1208_10-unsat.opb	j120	22022	69222	TO	UNK	T	10.35	T	360	0	0	0	481112	2321382
normalized-j1209_4-sat.opb	j120	21296	66999	FIN	SAT	131.82	10.16	121.61	348	0	0	0	470390	2270622
normalized-j301_4-unsat.opb	j30	3844	11854	FIN	UNSAT	4.60	4.29	0.29	183	0	0	0	14214	57726
normalized-j3020_1-sat.opb	j30	3596	11581	FIN	SAT	5.44	4.88	0.54	228	0	0	0	20924	89671
normalized-j3024_4-sat.opb	j30	3348	10816	FIN	SAT	5.75	4.83	0.90	212	0	0	0	57408	266435
normalized-j3025_1-sat.opb	j30	5828	19158	FIN	SAT	7.02	5.24	1.75	372	0	0	0	72416	333219
normalized-j3025_7-sat.opb	j30	5952	19548	FIN	SAT	7.69	5.49	2.17	380	0	0	0	79482	367153
normalized-j3027_8-sat.opb	j30	4154	13519	FIN	SAT	6.35	5.06	1.26	264	0	0	0	85268	400675
normalized-j3029_6-sat.opb	j30	5766	18893	FIN	SAT	27.85	5.82	21.99	368	0	0	0	119938	566201
normalized-j3029_8-unsat.opb	j30	4960	16157	FIN	UNSAT	44.84	5.81	39.00	316	0	0	0	114217	541270
normalized-j3031_7-sat.opb	j30	3844	12376	FIN	SAT	7.37	5.69	1.66	244	0	0	0	132737	636101
normalized-j3037_5-sat.opb	j30	5022	17060	FIN	SAT	6.22	5.26	0.94	320	0	0	0	39502	176420
normalized-j3041_4-unsat.opb	j30	4836	16649	FIN	UNSAT	6.12	5.03	1.06	308	0	0	0	64588	299470
normalized-j3046_4-unsat.opb	j30	3968	13430	FIN	UNSAT	7.49	6.13	1.33	252	0	0	0	120203	575831
normalized-j3048_8-sat.opb	j30	2790	9355	FIN	SAT	6.81	5.42	1.37	176	0	0	0	120886	582851
normalized-j308_1-unsat.opb	j30	2728	8382	FIN	UNSAT	5.20	4.95	0.23	172	0	0	0	40267	184596
normalized-j308_6-sat.opb	j30	2976	9039	FIN	SAT	5.45	4.60	0.83	188	0	0	0	55099	256353
normalized-j309_10-unsat.opb	j30	5456	17015	FIN	UNSAT	7.49	5.70	1.76	348	0	0	0	74273	342569
normalized-j309_9-sat.opb	j30	3968	12403	FIN	SAT	6.58	5.02	1.54	252	0	0	0	54305	250795
normalized-j6010_2-unsat.opb	j60	7564	23412	FIN	UNSAT	7.69	7.01	0.64	244	0	0	0	326716	1588733
normalized-j6013_2-unsat.opb	j60	12322	38967	TO	UNK	T	8.78	T	400	0	0	0	353922	1705167
normalized-j6015_4-sat.opb	j60	9272	28866	FIN	SAT	18.36	9.49	8.83	300	0	0	0	657947	3224991
normalized-j6018_3-sat.opb	j60	9516	31278	FIN	SAT	6.79	5.63	1.12	308	0	0	0	50403	222161
normalized-j6022_1-sat.opb	j60	7930	25932	FIN	SAT	7.48	5.56	1.88	256	0	0	0	137978	655244
normalized-j6027_4-unsat.opb	j60	7320	23840	FIN	UNSAT	8.24	7.60	0.62	236	0	0	0	330640	1610409
normalized-j602_7-unsat.opb	j60	6466	19939	FIN	UNSAT	5.51	4.96	0.52	208	0	0	0	46714	209947
normalized-j6030_9-unsat.opb	j60	11956	39426	FIN	UNSAT	10.62	9.78	0.80	388	0	0	0	504037	2452883
normalized-j603_2-unsat.opb	j60	8418	26241	FIN	UNSAT	6.21	5.74	0.44	272	0	0	0	62274	280425
normalized-j6033_2-unsat.opb	j60	12200	42056	FIN	UNSAT	6.44	5.87	0.53	396	0	0	0	52295	226691
normalized-j6035_10-sat.opb	j60	8784	30004	FIN	SAT	6.69	5.52	1.13	284	0	0	0	58058	261464
normalized-j6040_1-sat.opb	j60	10614	36312	FIN	SAT	10.47	7.50	2.93	344	0	0	0	244362	1171426
normalized-j6041_4-sat.opb	j60	16348	56848	FIN	SAT	18.84	6.86	11.92	532	0	0	0	255482	1211155
normalized-j6048_4-sat.opb	j60	7686	26213	FIN	SAT	14.95	9.14	5.77	248	0	0	0	581000	2852731
normalized-j605_10-unsat.opb	j60	9638	30220	FIN	UNSAT	40.91	6.27	34.60	312	0	0	0	120632	563896
normalized-j605_1-unsat.opb	j60	9272	29174	FIN	UNSAT	18.60	4.58	13.98	300	0	0	0	102947	477974
normalized-j605_7-sat.opb	j60	9272	29130	FIN	SAT	8.17	5.53	2.61	300	0	0	0	91772	422955
normalized-j606_1-unsat.opb	j60	7320	22689	FIN	UNSAT	6.12	5.60	0.50	236	0	0	0	129155	612689
normalized-j9010_6-unsat.opb	j90	16744	52975	FIN	UNSAT	12.82	11.73	1.04	364	0	0	0	720083	3517527
normalized-j9010_8-sat.opb	j90	14924	46875	FIN	SAT	24.28	10.34	13.89	324	0	0	0	557300	2715096
normalized-j9012_2-unsat.opb	j90	12922	40512	FIN	UNSAT	13.11	11.92	1.14	280	0	0	0	1258782	6203942
normalized-j9012_5-sat.opb	j90	15288	48064	FIN	SAT	18.56	15.06	3.44	332	0	0	0	1410103	6948352
normalized-j9014_1-unsat.opb	j90	16198	50975	FIN	UNSAT	15.44	14.30	1.08	352	0	0	0	1127374	5542439
normalized-j9015_10-unsat.opb	j90	14196	44553	FIN	UNSAT	15.44	14.16	1.22	308	0	0	0	1239420	6107225
normalized-j9027_5-sat.opb	j90	18200	60215	FIN	SAT	18.22	11.64	6.52	396	0	0	0	982559	4816571
normalized-j9028_2-unsat.opb	j90	13832	45398	FIN	UNSAT	13.89	12.78	1.07	300	0	0	0	1081532	5323823
normalized-j903_10-unsat.opb	j90	11830	36862	FIN	UNSAT	6.50	5.86	0.59	256	0	0	0	114294	530622
normalized-j9035_1-unsat.opb	j90	17836	61428	FIN	UNSAT	8.76	7.74	0.97	388	0	0	0	155867	724617
normalized-j9035_5-sat.opb	j90	18928	65252	FIN	SAT	9.71	7.41	2.24	412	0	0	0	147060	679544
normalized-j9039_3-unsat.opb	j90	15106	51849	FIN	UNSAT	9.33	8.52	0.76	328	0	0	0	402392	1948673
normalized-j9042_5-sat.opb	j90	19292	66786	FIN	SAT	24.18	11.73	12.37	420	0	0	0	663887	3235476
normalized-j9043_2-sat.opb	j90	16744	57767	FIN	SAT	19.82	11.77	7.99	364	0	0	0	759668	3717514
normalized-j9048_1-unsat.opb	j90	15106	51743	FIN	UNSAT	20.58	18.91	1.61	328	0	0	0	1968346	9733319
normalized-j906_2-sat.opb	j90	15834	49853	FIN	SAT	11.83	7.03	4.76	344	0	0	0	361726	1741387
normalized-j907_8-unsat.opb	j90	10920	34033	FIN	UNSAT	7.26	6.48	0.74	236	0	0	0	408698	1988644
normalized-neos808444.opb	neos	19846	18245	FIN	SAT	13.15	7.83	5.27	4717	0	0	396	217007	909101
normalized-neos-820146.opb	neos	600	830	TO	UNK	T	1.27	T	60	45	0	0	1965	6870
normalized-neos-820157.opb	neos	1200	1015	TO	UNK	T	1.64	T	85	45	0	0	4170	14315
normalized-neos-849702.opb	neos	1737	1041	FIN	SAT	91.60	5.11	86.47	1041	0	83	0	51019	223602
normalized-ooo.burch_dill.2.accl.ucl.opb	ooo	2152	5613	FIN	UNSAT	4.45	3.46	0.97	187	289	0	0	21525	90586
normalized-ooo.burch_dill.3.accl.ucl.opb	ooo	4622	12569	FIN	UNSAT	7.76	5.19	2.54	292	524	0	0	35348	147375
normalized-ooo.burch_dill.4.accl.ucl.opb	ooo	3939	10412	FIN	UNSAT	6.04	5.24	0.78	191	481	0	0	45138	193169
normalized-ooo.burch_dill.6.accl.ucl.opb	ooo	23621	67526	TO	UNK	T	9.38	T	718	1682	0	0	182625	773022
normalized-ooo.burch_dill.8.accl.ucl.opb	ooo	21380	60984	FIN	UNSAT	170.51	6.97	163.48	551	1605	0	0	143735	603899
normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb	ooo	49621	138346	FIN	UNSAT	233.77	32.17	201.48	5599	5357	0	0	2008500	8869651
normalized-ooo.ex.br.mem.Src1Valid_Src1ValidBar.ucl.opb	ooo	109757	313451	TO	UNK	T	61.41	T	9016	8506	10	0	4085165	18060817
normalized-ooo.ex.mem.LdValue.ucl.opb	ooo	77106	218779	TO	UNK	T	40.68	T	6748	6472	0	0	2491778	10983011
normalized-ooo.ex.mem.LsqHdStrong.ucl.opb	ooo	168111	487525	TO	UNK	T	67.85	T	9402	9396	4	0	4051515	17816785
normalized-ooo.rf10.ucl.opb	ooo	18069	52475	FIN	UNSAT	7.96	5.24	2.67	397	523	0	0	66732	266524
normalized-ooo.rf6.ucl.opb	ooo	1804	4931	FIN	UNSAT	5.18	4.93	0.22	103	121	0	0	7871	31154
normalized-ooo.rf7.ucl.opb	ooo	3736	10457	FIN	UNSAT	6.00	5.48	0.50	166	202	0	0	22848	94433
normalized-ooo.rf8.ucl.opb	ooo	6832	19477	FIN	UNSAT	6.46	5.67	0.76	232	292	0	0	33264	135597
normalized-ooo.rf9.ucl.opb	ooo	11476	33090	FIN	UNSAT	5.59	4.45	1.10	309	399	0	0	46373	186377
normalized-ooo.tag10.ucl.opb	ooo	9071	25914	FIN	UNSAT	7.01	5.70	1.27	299	425	0	0	45680	186945
normalized-ooo.tag12.ucl.opb	ooo	20605	59851	FIN	UNSAT	9.73	7.68	2.00	480	696	0	0	79271	317901
normalized-ooo.tag14.ucl.opb	ooo	40605	118930	FIN	UNSAT	16.73	10.99	5.65	705	1035	0	0	195474	806037
normalized-ooo.tag8.ucl.opb	ooo	3249	8983	FIN	UNSAT	5.24	4.64	0.58	162	222	0	0	21071	87233
normalized-ooo.unbounded.all.ucl.opb	ooo	84836	245062	FIN	UNSAT	728.86	44.63	684.03	5742	5722	0	0	2633874	11624524
normalized-pigeon-cardinality-101-100.opb	pig-card	10100	201	TO	UNK	T	4.69	T	100	0	0	0	30200	90201
normalized-pigeon-cardinality-105-100.opb	pig-card	10500	205	TO	UNK	T	4.96	T	100	0	0	0	31400	93805
normalized-pigeon-cardinality-11-10.opb	pig-card	110	21	FIN	UNSAT	1.36	0.23	1.11	10	0	0	0	320	921
normalized-pigeon-cardinality-15-10.opb	pig-card	150	25	FIN	UNSAT	1.16	0.42	0.72	10	0	0	0	440	1285
normalized-pigeon-cardinality-21-20.opb	pig-card	420	41	TO	UNK	T	1.56	T	20	0	0	0	1240	3641
normalized-pigeon-cardinality-25-20.opb	pig-card	500	45	TO	UNK	T	1.17	T	20	0	0	0	1480	4365
normalized-pigeon-cardinality-31-30.opb	pig-card	930	61	TO	UNK	T	2.56	T	30	0	0	0	2760	8161
normalized-pigeon-cardinality-35-30.opb	pig-card	1050	65	TO	UNK	T	1.58	T	30	0	0	0	3120	9245
normalized-pigeon-cardinality-41-40.opb	pig-card	1640	81	TO	UNK	T	2.62	T	40	0	0	0	4880	14481
normalized-pigeon-cardinality-45-40.opb	pig-card	1800	85	TO	UNK	T	2.97	T	40	0	0	0	5360	15925
normalized-pigeon-cardinality-51-50.opb	pig-card	2550	101	TO	UNK	T	1.90	T	50	0	0	0	7600	22601
normalized-pigeon-cardinality-55-50.opb	pig-card	2750	105	TO	UNK	T	1.90	T	50	0	0	0	8200	24405
normalized-pigeon-cardinality-61-60.opb	pig-card	3660	121	TO	UNK	T	2.35	T	60	0	0	0	10920	32521
normalized-pigeon-cardinality-65-60.opb	pig-card	3900	125	TO	UNK	T	2.40	T	60	0	0	0	11640	34685
normalized-pigeon-cardinality-71-70.opb	pig-card	4970	141	TO	UNK	T	3.97	T	70	0	0	0	14840	44241
normalized-pigeon-cardinality-75-70.opb	pig-card	5250	145	TO	UNK	T	3.87	T	70	0	0	0	15680	46765
normalized-pigeon-cardinality-81-80.opb	pig-card	6480	161	TO	UNK	T	4.98	T	80	0	0	0	19360	57761
normalized-pigeon-cardinality-85-80.opb	pig-card	6800	165	TO	UNK	T	4.51	T	80	0	0	0	20320	60645
normalized-pigeon-cardinality-91-90.opb	pig-card	8190	181	TO	UNK	T	5.24	T	90	0	0	0	24480	73081
normalized-pigeon-cardinality-95-90.opb	pig-card	8550	185	TO	UNK	T	5.12	T	90	0	0	0	25560	76325
normalized-pigeon-clauses-101-100.opb	pig-cl	10100	505101	TO	UNK	T	14.43	T	0	0	0	0	10100	505101
normalized-pigeon-clauses-105-100.opb	pig-cl	10500	546105	TO	UNK	T	17.20	T	0	0	0	0	10500	546105
normalized-pigeon-clauses-11-10.opb	pig-cl	110	561	FIN	UNSAT	66.26	0.46	65.78	0	0	0	0	110	561
normalized-pigeon-clauses-15-10.opb	pig-cl	150	1065	FIN	UNSAT	197.02	1.41	195.60	0	0	0	0	150	1065
normalized-pigeon-clauses-21-20.opb	pig-cl	420	4221	TO	UNK	T	3.03	T	0	0	0	0	420	4221
normalized-pigeon-clauses-25-20.opb	pig-cl	500	6025	TO	UNK	T	3.15	T	0	0	0	0	500	6025
normalized-pigeon-clauses-31-30.opb	pig-cl	930	13981	TO	UNK	T	3.06	T	0	0	0	0	930	13981
normalized-pigeon-clauses-35-30.opb	pig-cl	1050	17885	TO	UNK	T	3.33	T	0	0	0	0	1050	17885
normalized-pigeon-clauses-41-40.opb	pig-cl	1640	32841	TO	UNK	T	4.88	T	0	0	0	0	1640	32841
normalized-pigeon-clauses-45-40.opb	pig-cl	1800	39645	TO	UNK	T	4.86	T	0	0	0	0	1800	39645
normalized-pigeon-clauses-51-50.opb	pig-cl	2550	63801	TO	UNK	T	4.42	T	0	0	0	0	2550	63801
normalized-pigeon-clauses-55-50.opb	pig-cl	2750	74305	TO	UNK	T	4.65	T	0	0	0	0	2750	74305
normalized-pigeon-clauses-61-60.opb	pig-cl	3660	109861	TO	UNK	T	5.58	T	0	0	0	0	3660	109861
normalized-pigeon-clauses-65-60.opb	pig-cl	3900	124865	TO	UNK	T	5.66	T	0	0	0	0	3900	124865
normalized-pigeon-clauses-71-70.opb	pig-cl	4970	174021	TO	UNK	T	8.25	T	0	0	0	0	4970	174021
normalized-pigeon-clauses-75-70.opb	pig-cl	5250	194325	TO	UNK	T	8.72	T	0	0	0	0	5250	194325
normalized-pigeon-clauses-81-80.opb	pig-cl	6480	259281	TO	UNK	T	10.38	T	0	0	0	0	6480	259281
normalized-pigeon-clauses-85-80.opb	pig-cl	6800	285685	TO	UNK	T	11.29	T	0	0	0	0	6800	285685
normalized-pigeon-clauses-91-90.opb	pig-cl	8190	368641	TO	UNK	T	13.28	T	0	0	0	0	8190	368641
normalized-pigeon-clauses-95-90.opb	pig-cl	8550	401945	TO	UNK	T	14.14	T	0	0	0	0	8550	401945
normalized-ppp1-11-19-21.opb	ppp	4602	30179	TO	UNK	T	7.35	T	1019	0	0	0	30427	145640
normalized-ppp1-12-16.opb	ppp	4662	31725	FIN	SAT	8.02	7.11	0.87	1029	0	0	0	30831	148626
normalized-ppp1-13.opb	ppp	4632	30964	FIN	SAT	7.80	6.82	0.94	1024	0	0	0	31028	149134
normalized-ppp1-3-13-19.opb	ppp	4608	30348	FIN	SAT	8.88	7.28	1.58	1020	0	0	0	30714	147180
normalized-ppp1-9-16-19.opb	ppp	4626	30747	TO	UNK	T	6.81	T	1023	0	0	0	29697	142374
normalized-ppp3-13-25-26.opb	ppp	4644	31254	FIN	SAT	16.12	7.27	8.81	1026	0	0	0	31092	149640
normalized-robin10.opb	robin	2025	410	FIN	SAT	6.28	5.31	0.95	230	0	9	0	29894	126701
normalized-robin12.opb	robin	4356	600	FIN	SAT	20.63	4.62	15.99	336	0	10	0	64662	274650
normalized-robin14.opb	robin	8281	826	TO	UNK	T	7.92	T	462	0	12	0	123257	524180
normalized-robin16.opb	robin	14400	1088	TO	UNK	T	11.26	T	608	0	14	0	214730	913916
normalized-robin18.opb	robin	23409	1386	TO	UNK	T	16.77	T	774	0	18	0	349483	1488240
normalized-robin8.opb	robin	784	256	FIN	SAT	2.24	1.91	0.31	144	0	7	0	11465	48392
normalized-t2001.13queen13.1110966483.opb	13queen	169	101	FIN	UNSAT	3.04	1.40	1.62	65	2	0	0	5751	26864
normalized-t2001.13queen13.1110966688.opb	13queen	169	101	FIN	UNSAT	4.87	1.59	3.26	65	2	0	0	5948	27849
normalized-t2001.13queen13.1110967142.opb	13queen	169	101	FIN	UNSAT	8.58	1.33	7.24	65	2	0	0	6212	29169
normalized-t2001.13queen13.1110967327.opb	13queen	169	101	FIN	SAT	4.21	1.43	2.76	65	2	0	0	6200	29109
normalized-t2001.13queen13.1110967523.opb	13queen	169	101	FIN	UNSAT	6.21	1.38	4.81	65	2	0	0	6139	28804
normalized-t2001.13queen13.1110967729.opb	13queen	169	101	FIN	UNSAT	3.28	1.40	1.86	65	2	0	0	5634	26279
normalized-t2001.13queen13.1110968094.opb	13queen	169	101	FIN	UNSAT	5.40	1.65	3.73	65	2	0	0	5961	27914
normalized-t2001.13queen13.1110968431.opb	13queen	169	101	FIN	SAT	2.39	1.50	0.87	65	2	0	0	5883	27524
normalized-t2001.13queen13.1110968561.opb	13queen	169	101	FIN	UNSAT	6.49	1.42	5.05	65	2	0	0	5951	27864
normalized-t2001.13queen13.1110968898.opb	13queen	169	101	FIN	UNSAT	6.43	1.65	4.76	65	2	0	0	5927	27744
normalized-t2001.13queen13.1110969170.opb	13queen	169	101	FIN	UNSAT	5.01	1.39	3.60	65	2	0	0	6112	28669
normalized-t2001.13queen13.1110969577.opb	13queen	169	101	FIN	UNSAT	4.41	1.50	2.89	65	2	0	0	5961	27914
normalized-t2001.13queen13.1110969860.opb	13queen	169	101	FIN	UNSAT	8.04	1.61	6.41	65	2	0	0	6320	29709
normalized-t2001.13queen13.1110969933.opb	13queen	169	101	FIN	SAT	3.15	1.43	1.70	65	2	0	0	5890	27559
normalized-t2001.13queen13.1110970170.opb	13queen	169	101	FIN	SAT	4.20	1.42	2.76	65	2	0	0	6141	28814
normalized-t2001.13queen13.1110970277.opb	13queen	169	101	FIN	SAT	3.47	1.48	1.97	65	2	0	0	6266	29439
normalized-t2001.13queen13.1110970444.opb	13queen	169	101	FIN	UNSAT	3.56	1.43	2.11	65	2	0	0	6047	28344
normalized-t2001.13queen13.1110970631.opb	13queen	169	101	FIN	UNSAT	3.81	1.49	2.30	65	2	0	0	5712	26669
normalized-t2001.13queen13.1110971097.opb	13queen	169	101	FIN	SAT	5.69	1.54	4.13	65	2	0	0	6282	29519
normalized-t2001.13queen13.1110971363.opb	13queen	169	101	FIN	UNSAT	4.60	1.66	2.92	65	2	0	0	6103	28624
normalized-t2001.13queen13.1110971697.opb	13queen	169	101	FIN	UNSAT	5.35	1.69	3.64	65	2	0	0	6007	28144
normalized-t2001.13queen13.1110971766.opb	13queen	169	101	FIN	SAT	3.05	2.26	0.77	65	2	0	0	5970	27959
normalized-t2001.13queen13.1110972154.opb	13queen	169	101	FIN	UNSAT	5.93	1.54	4.36	65	2	0	0	6041	28314
normalized-t2001.13queen13.1110972763.opb	13queen	169	101	FIN	UNSAT	5.40	1.36	4.02	65	2	0	0	6074	28479
normalized-t2001.13queen13.1110972958.opb	13queen	169	101	FIN	SAT	2.01	1.38	0.61	65	2	0	0	6168	28949
normalized-t2001.13queen13.1110973163.opb	13queen	169	101	FIN	UNSAT	8.06	1.46	6.58	65	2	0	0	6128	28749
normalized-t2001.13queen13.1110973364.opb	13queen	169	101	FIN	UNSAT	4.15	1.35	2.78	65	2	0	0	5977	27994
normalized-t2001.13queen13.1110973478.opb	13queen	169	101	FIN	SAT	4.73	1.42	3.29	65	2	0	0	6093	28574
normalized-t2001.13queen13.1110973670.opb	13queen	169	101	FIN	UNSAT	5.71	1.42	4.27	65	2	0	0	5919	27704
normalized-t2001.13queen13.1110973863.opb	13queen	169	101	FIN	SAT	7.75	1.73	6.00	65	2	0	0	6038	28299
normalized-t2001.13queen13.1110974180.opb	13queen	169	101	FIN	UNSAT	6.95	2.25	4.67	65	2	0	0	6003	28124
normalized-t2001.13queen13.1110974372.opb	13queen	169	101	FIN	UNSAT	3.83	1.48	2.33	65	2	0	0	5983	28024
normalized-t2001.13queen13.1110974553.opb	13queen	169	101	FIN	SAT	4.00	2.33	1.65	65	2	0	0	6208	29149
normalized-t2001.13queen13.1110975607.opb	13queen	169	101	FIN	UNSAT	3.41	1.34	2.05	65	2	0	0	6019	28204
normalized-t2001.13queen13.1110975678.opb	13queen	169	101	FIN	SAT	3.20	1.33	1.85	65	2	0	0	6098	28599
normalized-t2001.13queen13.1110975832.opb	13queen	169	101	FIN	SAT	4.79	1.50	3.27	65	2	0	0	6250	29359
normalized-t2001.13queen13.1110975965.opb	13queen	169	101	FIN	UNSAT	9.50	1.45	8.03	65	2	0	0	6258	29399
normalized-t2001.13queen13.1110976157.opb	13queen	169	101	FIN	UNSAT	3.46	1.47	1.97	65	2	0	0	5834	27279
normalized-t2001.13queen13.1110976730.opb	13queen	169	101	FIN	UNSAT	9.29	1.49	7.78	65	2	0	0	6186	29039
normalized-t2001.13queen13.1110976735.opb	13queen	169	101	FIN	SAT	3.38	1.68	1.68	65	2	0	0	6340	29809
normalized-t2001.13queen13.1110976935.opb	13queen	169	101	FIN	UNSAT	3.92	1.29	2.61	65	2	0	0	6008	28149
normalized-t2001.13queen13.1110977266.opb	13queen	169	101	FIN	SAT	4.36	1.66	2.68	65	2	0	0	6035	28284
normalized-t2001.13queen13.1110977273.opb	13queen	169	101	FIN	UNSAT	5.61	1.34	4.25	65	2	0	0	5984	28029
normalized-t2001.13queen13.1110977464.opb	13queen	169	101	FIN	SAT	8.65	1.64	6.99	65	2	0	0	6104	28629
normalized-t2001.13queen13.1110977780.opb	13queen	169	101	FIN	UNSAT	3.99	1.49	2.48	65	2	0	0	5763	26924
normalized-t2001.13queen13.1110978113.opb	13queen	169	101	FIN	UNSAT	7.58	1.45	6.11	65	2	0	0	6121	28714
normalized-t2001.13queen13.1110978334.opb	13queen	169	101	FIN	UNSAT	5.16	2.32	2.82	65	2	0	0	6017	28194
normalized-t2001.13queen13.1111212272.opb	13queen	169	101	FIN	UNSAT	6.20	1.45	4.73	65	2	0	0	6096	28589
normalized-t2001.13queen13.1111212476.opb	13queen	169	101	FIN	UNSAT	7.32	1.42	5.88	65	2	0	0	6309	29654
normalized-t2001.13queen13.1111212923.opb	13queen	169	101	FIN	UNSAT	4.92	1.56	3.34	65	2	0	0	6004	28129
normalized-t2001.13queen13.1111213670.opb	13queen	169	101	FIN	UNSAT	4.82	1.69	3.11	65	2	0	0	6130	28759
normalized-t2001.13queen13.1111213868.opb	13queen	169	101	FIN	UNSAT	5.38	1.61	3.74	65	2	0	0	6211	29164
normalized-t2001.13queen13.1111216188.opb	13queen	169	101	FIN	SAT	2.76	1.46	1.28	65	2	0	0	6071	28464
normalized-t2001.13queen13.1111216411.opb	13queen	169	101	FIN	UNSAT	6.16	1.49	4.65	65	2	0	0	6032	28269
normalized-t2001.13queen13.1111216823.opb	13queen	169	101	FIN	UNSAT	5.32	1.56	3.74	65	2	0	0	6067	28444
normalized-t2001.13queen13.1111216864.opb	13queen	169	101	FIN	SAT	4.07	1.60	2.45	65	2	0	0	6047	28344
normalized-t2001.13queen13.1111217374.opb	13queen	169	101	FIN	SAT	1.98	1.59	0.37	65	2	0	0	6336	29789
normalized-t2001.13queen13.1111217380.opb	13queen	169	101	FIN	SAT	2.39	1.67	0.70	65	2	0	0	6147	28844
normalized-t2001.13queen13.1111217392.opb	13queen	169	101	FIN	UNSAT	4.54	1.50	3.02	65	2	0	0	5949	27854
normalized-t2001.13queen13.1111217555.opb	13queen	169	101	FIN	UNSAT	6.44	2.09	4.33	65	2	0	0	5998	28099
normalized-t2001.13queen13.1111218024.opb	13queen	169	101	FIN	UNSAT	5.27	1.53	3.72	65	2	0	0	6032	28269
normalized-t2001.13queen13.1111218308.opb	13queen	169	101	FIN	UNSAT	12.00	1.60	10.37	65	2	0	0	6239	29304
normalized-t2001.13queen13.1111218757.opb	13queen	169	101	FIN	UNSAT	6.36	1.69	4.65	65	2	0	0	5969	27954
normalized-t2001.13queen13.1111218955.opb	13queen	169	101	FIN	UNSAT	4.12	1.44	2.66	65	2	0	0	6122	28719
normalized-t2001.13queen13.1111219348.opb	13queen	169	101	FIN	UNSAT	5.11	1.76	3.33	65	2	0	0	6083	28524
normalized-t2001.13queen13.1111219399.opb	13queen	169	101	FIN	SAT	2.13	1.45	0.67	65	2	0	0	6059	28404
normalized-t2001.13queen13.1111219799.opb	13queen	169	101	FIN	UNSAT	4.04	1.46	2.55	65	2	0	0	5938	27799
normalized-t2001.13queen13.1111220019.opb	13queen	169	101	FIN	UNSAT	4.82	1.52	3.28	65	2	0	0	5883	27524
normalized-t2001.13queen13.1111220546.opb	13queen	169	101	FIN	UNSAT	5.49	1.66	3.81	65	2	0	0	5928	27749
normalized-t2001.13queen13.1111220767.opb	13queen	169	101	FIN	UNSAT	6.12	1.64	4.46	65	2	0	0	5991	28064
normalized-t2001.13queen13.1111221203.opb	13queen	169	101	FIN	UNSAT	5.45	1.25	4.18	65	2	0	0	5973	27974
normalized-t2001.13queen13.1111221624.opb	13queen	169	101	FIN	UNSAT	5.56	1.67	3.86	65	2	0	0	6027	28244
normalized-t2001.13queen13.1111221953.opb	13queen	169	101	FIN	SAT	2.88	1.44	1.42	65	2	0	0	5875	27484
normalized-t2001.13queen13.1111222080.opb	13queen	169	101	FIN	SAT	5.70	1.55	4.13	65	2	0	0	6012	28169
normalized-t2001.13queen13.1111222248.opb	13queen	169	101	FIN	SAT	3.24	1.45	1.77	65	2	0	0	6311	29664
normalized-t2001.13queen13.1111222257.opb	13queen	169	101	FIN	UNSAT	4.84	1.55	3.28	65	2	0	0	5989	28054
normalized-t2001.13queen13.1111222539.opb	13queen	169	101	FIN	UNSAT	6.35	1.51	4.82	65	2	0	0	6216	29189
normalized-t2001.13queen13.1111223004.opb	13queen	169	101	FIN	UNSAT	7.02	1.45	5.55	65	2	0	0	5975	27984
normalized-t2001.13queen13.1111223220.opb	13queen	169	101	FIN	UNSAT	5.99	1.60	4.37	65	2	0	0	6040	28309
normalized-t2001.13queen13.1111223416.opb	13queen	169	101	FIN	SAT	2.90	2.30	0.58	65	2	0	0	6042	28319
normalized-t2001.13queen13.1111223596.opb	13queen	169	101	FIN	SAT	4.24	1.45	2.76	65	2	0	0	5961	27914
normalized-t2001.13queen13.1111223689.opb	13queen	169	101	FIN	SAT	1.74	1.52	0.20	65	2	0	0	6215	29184
normalized-t2001.13queen13.1111223696.opb	13queen	169	101	FIN	SAT	2.55	1.64	0.89	65	2	0	0	5918	27699
normalized-t2001.13queen13.1111224059.opb	13queen	169	101	FIN	UNSAT	3.83	1.66	2.15	65	2	0	0	5750	26859
normalized-t2001.13queen13.1111224255.opb	13queen	169	101	FIN	UNSAT	5.69	1.66	4.01	65	2	0	0	6052	28369
normalized-t2001.13queen13.1111224451.opb	13queen	169	101	FIN	UNSAT	5.10	1.59	3.49	65	2	0	0	5939	27804
normalized-t2001.13queen13.1111224522.opb	13queen	169	101	FIN	SAT	2.84	1.71	1.11	65	2	0	0	5851	27364
normalized-t2001.13queen13.1111224929.opb	13queen	169	101	FIN	UNSAT	3.98	1.46	2.49	65	2	0	0	5889	27554
normalized-t2001.13queen13.1111225122.opb	13queen	169	101	FIN	UNSAT	3.79	1.65	2.12	65	2	0	0	5939	27804
normalized-t2001.13queen13.1111225605.opb	13queen	169	101	FIN	UNSAT	4.54	1.41	3.11	65	2	0	0	6005	28134
normalized-t2001.13queen13.1111226062.opb	13queen	169	101	FIN	UNSAT	4.51	1.64	2.85	65	2	0	0	5957	27894
normalized-t2001.13queen13.1111226241.opb	13queen	169	101	FIN	SAT	2.48	1.50	0.97	65	2	0	0	6209	29154
normalized-t2001.13queen13.1111226284.opb	13queen	169	101	FIN	SAT	4.76	1.68	3.06	65	2	0	0	6128	28749
normalized-t2001.13queen13.1111226368.opb	13queen	169	101	FIN	UNSAT	4.56	1.65	2.89	65	2	0	0	5863	27424
normalized-t2001.13queen13.1111226680.opb	13queen	169	101	FIN	UNSAT	6.52	1.51	4.99	65	2	0	0	6178	28999
normalized-t2001.13queen13.1111227012.opb	13queen	169	101	FIN	UNSAT	5.93	1.73	4.18	65	2	0	0	6030	28259
normalized-t2001.13queen13.1111227326.opb	13queen	169	101	FIN	UNSAT	3.57	1.66	1.89	65	2	0	0	5918	27699
normalized-t2001.13queen13.1111227418.opb	13queen	169	101	FIN	SAT	3.94	1.61	2.31	65	2	0	0	6118	28699
normalized-t2001.13queen13.1111227861.opb	13queen	169	101	FIN	UNSAT	4.81	1.66	3.13	65	2	0	0	5917	27694
normalized-t2001.13queen13.1111228076.opb	13queen	169	101	FIN	UNSAT	7.90	1.76	6.12	65	2	0	0	6021	28214
normalized-t3002.11tsp11.1900544463.opb	11tsp11	231	2707	FIN	SAT	4.37	3.63	0.72	23	0	0	0	2650	14310
normalized-t3002.11tsp11.1900544484.opb	11tsp11	231	2707	FIN	UNSAT	19.29	3.81	15.46	23	0	0	0	2418	13150
normalized-t3002.11tsp11.1900545610.opb	11tsp11	231	2707	FIN	UNSAT	36.97	4.06	32.89	23	0	0	0	2658	14350
normalized-t3002.11tsp11.1900546076.opb	11tsp11	231	2707	FIN	UNSAT	4.80	4.17	0.61	23	0	0	0	2542	13770
normalized-t3002.11tsp11.1900546417.opb	11tsp11	231	2707	FIN	UNSAT	26.13	4.02	22.09	23	0	0	0	2538	13750
normalized-t3002.11tsp11.1900547334.opb	11tsp11	231	2707	FIN	SAT	4.41	3.91	0.48	23	0	0	0	2622	14170
normalized-t3002.11tsp11.1900547353.opb	11tsp11	231	2707	FIN	SAT	4.22	3.90	0.30	23	0	0	0	2414	13130
normalized-t3002.11tsp11.1900547389.opb	11tsp11	231	2707	FIN	UNSAT	33.24	3.98	29.23	23	0	0	0	2552	13820
normalized-t3002.11tsp11.1900547416.opb	11tsp11	231	2707	FIN	SAT	2.47	2.11	0.34	23	0	0	0	2424	13180
normalized-t3002.11tsp11.1900547427.opb	11tsp11	231	2707	FIN	SAT	4.63	4.07	0.54	23	0	0	0	2660	14360
normalized-t3002.11tsp11.1900547461.opb	11tsp11	231	2707	FIN	SAT	4.16	3.76	0.38	23	0	0	0	2568	13900
normalized-t3002.11tsp11.1900548667.opb	11tsp11	231	2707	FIN	UNSAT	90.32	3.69	86.61	23	0	0	0	2752	14820
normalized-t3002.11tsp11.1900549974.opb	11tsp11	231	2707	FIN	SAT	4.56	3.72	0.82	23	0	0	0	2634	14230
normalized-t3002.11tsp11.1900550006.opb	11tsp11	231	2707	FIN	UNSAT	55.65	2.86	52.77	23	0	0	0	2628	14200
normalized-t3002.11tsp11.1900550720.opb	11tsp11	231	2707	FIN	UNSAT	46.55	3.56	42.97	23	0	0	0	2604	14080
normalized-t3002.11tsp11.1900551347.opb	11tsp11	231	2707	FIN	UNSAT	5.58	3.77	1.79	23	0	0	0	2456	13340
normalized-t3002.11tsp11.1900551864.opb	11tsp11	231	2707	FIN	UNSAT	9.41	3.93	5.46	23	0	0	0	2548	13800
normalized-t3002.11tsp11.1900552288.opb	11tsp11	231	2707	FIN	UNSAT	27.09	3.64	23.43	23	0	0	0	2506	13590
normalized-t3002.11tsp11.1900552311.opb	11tsp11	231	2707	FIN	SAT	3.03	2.80	0.21	23	0	0	0	2452	13320
normalized-t3002.11tsp11.1900552423.opb	11tsp11	231	2707	FIN	UNSAT	5.01	4.21	0.78	23	0	0	0	2342	12770
normalized-t3002.11tsp11.1900552735.opb	11tsp11	231	2707	FIN	UNSAT	5.01	3.80	1.19	23	0	0	0	2508	13600
normalized-t3002.11tsp11.1900553606.opb	11tsp11	231	2707	FIN	SAT	3.59	2.30	1.27	23	0	0	0	2644	14280
normalized-t3002.11tsp11.1900553644.opb	11tsp11	231	2707	FIN	SAT	4.05	3.86	0.17	23	0	0	0	2658	14350
normalized-t3002.11tsp11.1900553647.opb	11tsp11	231	2707	FIN	UNSAT	39.99	3.76	36.21	23	0	0	0	2526	13690
normalized-t3002.11tsp11.1900553812.opb	11tsp11	231	2707	FIN	UNSAT	4.88	3.89	0.97	23	0	0	0	2540	13760
normalized-t3002.11tsp11.1900554067.opb	11tsp11	231	2707	FIN	SAT	4.56	4.00	0.54	23	0	0	0	2790	15010
normalized-t3002.11tsp11.1900554072.opb	11tsp11	231	2707	FIN	UNSAT	24.14	3.73	20.39	23	0	0	0	2586	13990
normalized-t3002.11tsp11.1900554154.opb	11tsp11	231	2707	FIN	SAT	4.01	3.83	0.16	23	0	0	0	2676	14440
normalized-t3002.11tsp11.1900554373.opb	11tsp11	231	2707	FIN	SAT	4.12	3.92	0.18	23	0	0	0	2800	15060
normalized-t3002.11tsp11.1900554375.opb	11tsp11	231	2707	FIN	SAT	4.38	4.17	0.19	23	0	0	0	2668	14400
normalized-t3002.11tsp11.1900554389.opb	11tsp11	231	2707	FIN	SAT	4.23	3.82	0.38	23	0	0	0	2610	14110
normalized-t3002.11tsp11.1900554420.opb	11tsp11	231	2707	FIN	UNSAT	7.46	3.88	3.56	23	0	0	0	2598	14050
normalized-t3002.11tsp11.1900556231.opb	11tsp11	231	2707	FIN	UNSAT	22.24	3.90	18.32	23	0	0	0	2470	13410
normalized-t3002.11tsp11.1900557362.opb	11tsp11	231	2707	FIN	UNSAT	3.13	2.23	0.87	23	0	0	0	2592	14020
normalized-t3002.11tsp11.1900557413.opb	11tsp11	231	2707	FIN	SAT	4.58	3.84	0.71	23	0	0	0	2772	14920
normalized-t3002.11tsp11.1900557568.opb	11tsp11	231	2707	FIN	SAT	3.88	3.71	0.15	23	0	0	0	2804	15080
normalized-t3002.11tsp11.1900557574.opb	11tsp11	231	2707	FIN	UNSAT	11.16	4.58	6.55	23	0	0	0	2560	13860
normalized-t3002.11tsp11.1900557957.opb	11tsp11	231	2707	FIN	UNSAT	20.20	2.44	17.73	23	0	0	0	2536	13740
normalized-t3002.11tsp11.1900558106.opb	11tsp11	231	2707	FIN	UNSAT	4.69	4.36	0.31	23	0	0	0	2274	12430
normalized-t3002.11tsp11.1900558739.opb	11tsp11	231	2707	FIN	UNSAT	35.35	3.82	31.50	23	0	0	0	2662	14370
normalized-t3002.11tsp11.1900559365.opb	11tsp11	231	2707	FIN	SAT	4.49	3.95	0.51	23	0	0	0	2562	13870
normalized-t3002.11tsp11.1900559416.opb	11tsp11	231	2707	FIN	SAT	5.96	3.85	2.09	23	0	0	0	2668	14400
normalized-t3002.11tsp11.1900559641.opb	11tsp11	231	2707	FIN	SAT	4.97	4.65	0.30	23	0	0	0	2617	14145
normalized-t3002.11tsp11.1900559676.opb	11tsp11	231	2707	FIN	UNSAT	68.58	4.29	64.27	23	0	0	0	2762	14870
normalized-t3002.11tsp11.1900561288.opb	11tsp11	231	2707	FIN	UNSAT	94.03	2.25	91.76	23	0	0	0	2770	14910
normalized-t3002.11tsp11.1900561384.opb	11tsp11	231	2707	FIN	SAT	4.08	3.81	0.25	23	0	0	0	2880	15460
normalized-t3002.11tsp11.1900561389.opb	11tsp11	231	2707	FIN	SAT	4.55	3.70	0.83	23	0	0	0	2498	13550
normalized-t3002.11tsp11.1900562192.opb	11tsp11	231	2707	FIN	UNSAT	8.18	2.27	5.89	23	0	0	0	2394	13030
normalized-t3002.11tsp11.1900563250.opb	11tsp11	231	2707	FIN	UNSAT	24.09	2.32	21.75	23	0	0	0	2622	14170
normalized-t3002.11tsp11.1900563801.opb	11tsp11	231	2707	FIN	UNSAT	6.00	3.57	2.41	23	0	0	0	2492	13520
normalized-t3002.11tsp11.1900564281.opb	11tsp11	231	2707	FIN	UNSAT	5.58	3.93	1.63	23	0	0	0	2604	14080
normalized-t3002.11tsp11.1900564822.opb	11tsp11	231	2707	FIN	SAT	3.91	3.69	0.20	23	0	0	0	2734	14730
normalized-t3002.11tsp11.1900564824.opb	11tsp11	231	2707	FIN	UNSAT	4.36	3.58	0.76	23	0	0	0	2254	12330
normalized-t3002.11tsp11.1900565527.opb	11tsp11	231	2707	FIN	SAT	4.13	3.68	0.43	23	0	0	0	2478	13450
normalized-t3002.11tsp11.1900565534.opb	11tsp11	231	2707	FIN	UNSAT	21.12	3.77	17.33	23	0	0	0	2594	14030
normalized-t3002.11tsp11.1900566151.opb	11tsp11	231	2707	FIN	SAT	4.70	4.46	0.22	23	0	0	0	2616	14140
normalized-t3002.11tsp11.1900566157.opb	11tsp11	231	2707	FIN	UNSAT	13.88	3.44	10.42	23	0	0	0	2282	12470
normalized-t3002.11tsp11.1900566263.opb	11tsp11	231	2707	FIN	SAT	3.98	3.77	0.19	23	0	0	0	2776	14940
normalized-t3002.11tsp11.1900566270.opb	11tsp11	231	2707	FIN	SAT	4.06	3.81	0.23	23	0	0	0	2830	15210
normalized-t3002.11tsp11.1900567003.opb	11tsp11	231	2707	FIN	SAT	4.77	4.33	0.42	23	0	0	0	2498	13550
normalized-t3002.11tsp11.1900567024.opb	11tsp11	231	2707	FIN	UNSAT	4.01	2.20	1.79	23	0	0	0	2394	13030
normalized-t3002.11tsp11.1900567135.opb	11tsp11	231	2707	FIN	UNSAT	14.65	3.65	10.98	23	0	0	0	2416	13140
normalized-t3002.11tsp11.1900567939.opb	11tsp11	231	2707	FIN	SAT	3.82	3.64	0.16	23	0	0	0	2576	13940
normalized-t3002.11tsp11.1900567985.opb	11tsp11	231	2707	FIN	UNSAT	29.88	3.74	26.12	23	0	0	0	2634	14230
normalized-t3002.11tsp11.1900568186.opb	11tsp11	231	2707	FIN	UNSAT	6.66	3.89	2.75	23	0	0	0	2524	13680
normalized-t3002.11tsp11.1900568706.opb	11tsp11	231	2707	FIN	UNSAT	17.99	3.92	14.05	23	0	0	0	2580	13960
normalized-t3002.11tsp11.1900568952.opb	11tsp11	231	2707	FIN	SAT	4.03	3.67	0.34	23	0	0	0	2624	14180
normalized-t3002.11tsp11.1900569834.opb	11tsp11	231	2707	FIN	UNSAT	11.72	3.66	8.04	23	0	0	0	2518	13652
normalized-t3002.11tsp11.1900570242.opb	11tsp11	231	2707	FIN	UNSAT	7.61	3.74	3.85	23	0	0	0	2474	13430
normalized-t3002.11tsp11.1900571131.opb	11tsp11	231	2707	FIN	SAT	4.12	3.75	0.35	23	0	0	0	2648	14300
normalized-t3002.11tsp11.1900571132.opb	11tsp11	231	2707	FIN	UNSAT	46.04	3.80	42.22	23	0	0	0	2390	13010
normalized-t3002.11tsp11.1900571761.opb	11tsp11	231	2707	FIN	UNSAT	40.07	3.73	36.31	23	0	0	0	2526	13690
normalized-t3002.11tsp11.1900573137.opb	11tsp11	231	2707	FIN	UNSAT	27.44	2.22	25.20	23	0	0	0	2582	13970
normalized-t3002.11tsp11.1900573901.opb	11tsp11	231	2707	FIN	UNSAT	39.62	3.76	35.84	23	0	0	0	2548	13800
normalized-t3002.11tsp11.1900574864.opb	11tsp11	231	2707	FIN	UNSAT	11.38	3.51	7.84	23	0	0	0	2622	14170
normalized-t3002.11tsp11.1900574948.opb	11tsp11	231	2707	FIN	SAT	4.66	4.38	0.26	23	0	0	0	2592	14020
normalized-t3002.11tsp11.1900574974.opb	11tsp11	231	2707	FIN	SAT	3.82	3.62	0.18	23	0	0	0	2602	14070
normalized-t3002.11tsp11.1900575442.opb	11tsp11	231	2707	FIN	UNSAT	20.33	3.68	16.63	23	0	0	0	2600	14060
normalized-t3002.11tsp11.1900576151.opb	11tsp11	231	2707	FIN	UNSAT	45.59	2.21	43.36	23	0	0	0	2552	13820
normalized-t3002.11tsp11.1900576360.opb	11tsp11	231	2707	FIN	UNSAT	19.17	3.72	15.43	23	0	0	0	2466	13390
normalized-t3002.11tsp11.1900576918.opb	11tsp11	231	2707	FIN	SAT	4.12	3.72	0.38	23	0	0	0	2708	14600
normalized-t3002.11tsp11.1900576927.opb	11tsp11	231	2707	FIN	UNSAT	47.33	3.67	43.64	23	0	0	0	2622	14170
normalized-t3002.11tsp11.1900577000.opb	11tsp11	231	2707	FIN	SAT	2.46	2.23	0.21	23	0	0	0	2702	14570
normalized-t3002.11tsp11.1900577940.opb	11tsp11	231	2707	FIN	UNSAT	63.69	3.78	59.89	23	0	0	0	2608	14100
normalized-t3002.11tsp11.1900579996.opb	11tsp11	231	2707	FIN	UNSAT	65.00	3.80	61.18	23	0	0	0	2559	13855
normalized-t3002.11tsp11.1900581320.opb	11tsp11	231	2707	FIN	UNSAT	48.80	3.63	45.15	23	0	0	0	2688	14500
normalized-t3002.11tsp11.1900581321.opb	11tsp11	231	2707	FIN	SAT	4.25	4.04	0.19	23	0	0	0	2684	14480
normalized-t3002.11tsp11.1900582300.opb	11tsp11	231	2707	FIN	UNSAT	64.44	3.85	60.57	23	0	0	0	2650	14310
normalized-t3002.11tsp11.1900582376.opb	11tsp11	231	2707	FIN	SAT	3.92	3.63	0.27	23	0	0	0	2420	13160
normalized-t3002.11tsp11.1900583053.opb	11tsp11	231	2707	FIN	UNSAT	58.09	3.49	54.58	23	0	0	0	2676	14440
normalized-t3002.11tsp11.1900584106.opb	11tsp11	231	2707	FIN	UNSAT	3.98	2.20	1.76	23	0	0	0	2534	13730
normalized-t3002.11tsp11.1900584219.opb	11tsp11	231	2707	FIN	UNSAT	12.55	3.73	8.80	23	0	0	0	2612	14120
normalized-t3002.11tsp11.1900667195.opb	11tsp11	231	2707	FIN	UNSAT	46.50	3.78	42.70	23	0	0	0	2670	14410
normalized-t3002.11tsp11.1900669299.opb	11tsp11	231	2707	FIN	SAT	2.47	2.11	0.34	23	0	0	0	2534	13730
normalized-t3002.11tsp11.1900669309.opb	11tsp11	231	2707	FIN	SAT	3.94	2.28	1.64	23	0	0	0	2668	14400
normalized-t3002.11tsp11.1900669797.opb	11tsp11	231	2707	FIN	UNSAT	34.85	2.28	32.55	23	0	0	0	2582	13970
normalized-t3002.11tsp11.1900670167.opb	11tsp11	231	2707	FIN	UNSAT	22.89	2.55	20.32	23	0	0	0	2566	13890
normalized-t3002.11tsp11.1900670234.opb	11tsp11	231	2707	FIN	UNSAT	77.68	3.66	74.00	23	0	0	0	2734	14730
normalized-t3002.11tsp11.1900670675.opb	11tsp11	231	2707	FIN	UNSAT	8.51	3.91	4.59	23	0	0	0	2614	14130
normalized-t3002.11tsp11.1900670756.opb	11tsp11	231	2707	FIN	SAT	3.95	3.63	0.30	23	0	0	0	2588	14000
normalized-vdw_k3_l5_n550.opb	vdw	1650	113164	FIN	SAT	376.34	6.93	369.17	0	0	0	0	1650	114814
normalized-vdw_k3_l6_n1500.opb	vdw	4500	674250	FIN	SAT	96.80	41.73	53.70	0	0	0	0	4500	678750
normalized-vdw_k4_l4_n360.opb	vdw	1440	86040	TO	UNK	T	5.72	T	360	0	0	0	3960	96120
normalized-vdw_k5_l4_n750.opb	vdw	3750	467625	TO	UNK	T	20.88	T	750	0	0	0	10500	495375
normalized-vdw_k6_l3_n170.opb	vdw	1020	43010	TO	UNK	T	3.39	T	170	0	0	0	2890	50830

References

[AbioNORM12] Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Valentin Mayer-Eichberger. A New Look at BDDs for Pseudo-Boolean Constraints. Journal of Artificial Intelligence Research, 45:443-480, 2012.
[EenS06] Niklas Eén and Niklas Sörensson. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, 2006.
[BailleuxBR09] Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New encodings of pseudo-Boolean constraints into CNF. In Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), LNCS 5584, pages 181-194, 2009.
[ManquinhoS06] Vasco M. Manquinho and João P. Marques Silva. On using cutting planes in pseudo-Boolean optimization. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):209-219, 2006.
[BerreP10] Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7(2-3):59-6, 2010.
[ManquinhoML10] Vasco M. Manquinho, Ruben Martins, and Inês Lynce. Improving unsatisfiability-based algorithms for Boolean optimization. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT 2010), LNCS 6175, pages 181-193, 2010.
[SilverthornM10] Bryan Silverthorn and Risto Miikkulainen. Latent class models for algorithm portfolio methods. In Proceedings of the 24th National Conference on Artificial Intelligence (AAAI 2010), 2010.
[GebserKNS07] Martin Gebser, Benjamin Kaufmann, André Neumann, and Torsten Schaub. Conflict-driven answer set solving. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI 2007), AAAI Press/MIT Press, pages 386-392, 2007.

PBSugar: Experimental Results

Table of Contents

Overview

Machine Specification and Software Versions

Benchmark Instances

Results on Solving

Number of instances solved

Time spent for solving

Cactus Plot

Effect of Reusing/Sharing Counter Matrices

Number of instances solved

Time spent for solving

Raw Data

Table of PBSugar Raw Data

References