Mark Liffiton

About | Research | Publications | CAMUS - Benz w/ PCSes

CAMUS Results - Benz Benchmarks Using PCSes

These are the instances from the full set of automotive product configuration benchmarks that timed out in the first phase of CAMUS (finding MCSes). Here, we use these instances to illustrate relaxing the completeness criterion of CAMUS in order to deal with such intractable instances.

The idea behind this approach is to truncate MCSes found in the complete CAMUS algorithm to form PCSes instead. By controlling how much truncation is done, we can alter the number of PCSes found, and thus the number of MUSes and total runtime as well. Each of the three tables below contains results for running the algorithm with a limit set on the size of each PCS, from 1 to 3. (The Max PCS size is often above this limit due to the specifics of the algorithm; the limit is a fairly strict guide, but it is broken at times.) When the algorithm is run with a PCS size limit of 1, it always produces a single, exact MUS.

Runs that reached the 600 second timeout are indicated by "--". In these cases, either the number of PCSes or MUSes generated is preceded by a ">" indicating that this is the number found before the timeout was reached. If the MUS computation timed out, the Min and Max MUS sizes are the smallest and largest of those found before timing out - they are upper and lower bounds, respectively.

These data were generated on an older machine (2.2GHz Opteron) with an older, unreleased version of CAMUS. We are working on updating this to reflect newer data.

Size Limit = 1

			Runtimes (sec)				PCS sizes			MUS sizes
Name	Vars	Clauses	PCSes	MUSes	Total	#PCSes	Min	Max	MUSes	Min	Max
C168_FW_SZ_107	1583	5939	2.98	0.001	2.981	92	1	1	1	92	92
C168_FW_SZ_128	1583	4777	2.46	0.001	2.461	118	1	1	1	118	118
C168_FW_SZ_41	1583	4727	0.721	0	0.721	40	1	1	1	40	40
C168_FW_SZ_66	1583	4751	0.316	0	0.316	19	1	1	1	19	19
C168_FW_SZ_75	1583	4744	0.463	0	0.463	57	1	1	1	57	57
C168_FW_UT_2463	1804	6756	1.31	0.001	1.311	62	1	1	1	62	62
C168_FW_UT_2468	1804	6754	1.67	0.001	1.671	57	1	1	1	57	57
C168_FW_UT_2469	1804	6767	1.06	0.001	1.061	38	1	1	1	38	38
C168_FW_UT_714	1804	6754	0.077	0	0.077	9	1	1	1	9	9
C202_FS_SZ_74	1556	5561	0.504	0.001	0.505	182	1	1	1	182	182
C202_FS_SZ_84	1556	5479	9.22	0.001	9.221	234	1	1	1	234	234
C202_FW_SZ_100	1561	7484	0.825	0.001	0.826	27	1	1	1	27	27
C202_FW_SZ_103	1561	9024	25.2	0.001	25.201	292	1	1	1	292	292
C202_FW_SZ_61	1561	7490	1.72	0	1.72	44	1	1	1	44	44
C202_FW_SZ_77	1561	7611	0.882	0.001	0.883	184	1	1	1	184	184
C202_FW_SZ_87	1561	7696	31.1	0.002	31.102	398	1	1	1	398	398
C202_FW_SZ_96	1561	7599	13.1	0.001	13.101	236	1	1	1	236	236
C202_FW_SZ_98	1561	7438	0.814	0.001	0.815	29	1	1	1	29	29
C202_FW_UT_2814	1820	9957	7.06	0.001	7.061	47	1	1	1	47	47
C202_FW_UT_2815	1820	9957	6.98	0.001	6.981	47	1	1	1	47	47
C208_FC_RZ_65	1513	4491	0.167	0	0.167	12	1	1	1	12	12
C208_FC_SZ_107	1513	4554	0.68	0.001	0.681	70	1	1	1	70	70
C210_FS_RZ_23	1608	4911	0.523	0	0.523	39	1	1	1	39	39
C210_FS_SZ_103	1607	4915	0.886	0.001	0.887	57	1	1	1	57	57
C210_FS_SZ_55	1608	4917	0.729	0.001	0.73	59	1	1	1	59	59
C210_FS_SZ_78	1607	5071	0.588	0	0.588	187	1	1	1	187	187
C210_FW_RZ_30	1629	6407	0.804	0	0.804	45	1	1	1	45	45
C210_FW_SZ_106	1628	6405	1.99	0.001	1.991	74	1	1	1	74	74
C210_FW_SZ_128	1628	6401	0.385	0	0.385	30	1	1	1	30	30
C210_FW_SZ_80	1628	6560	0.56	0	0.56	174	1	1	1	174	174
C210_FW_SZ_90	1628	6977	17.2	0.001	17.201	299	1	1	1	299	299
C210_FW_SZ_91	1628	6709	16.3	0.001	16.301	302	1	1	1	302	302
C210_FW_UT_8630	1891	8511	1.3	0.001	1.301	35	1	1	1	35	35
C210_FW_UT_8634	1891	8504	2.97	0	2.97	42	1	1	1	42	42
C220_FV_SZ_39	1530	4788	11.8	0.001	11.801	309	1	1	1	309	309

Size Limit = 2

			Runtimes (sec)				PCS sizes			MUS sizes
Name	Vars	Clauses	PCSes	MUSes	Total	#PCSes	Min	Max	MUSes	Min	Max
C168_FW_SZ_107	1583	5939	29.6	0.057	29.657	434	1	3	2136	47	122
C168_FW_SZ_128	1583	4777	3.02	191	194.02	245	1	3	6268144	99	129
C168_FW_SZ_41	1583	4727	2.9	0.004	2.904	122	1	3	118	27	47
C168_FW_SZ_66	1583	4751	4.16	0.007	4.167	189	1	3	248	16	49
C168_FW_SZ_75	1583	4744	2.39	0.014	2.404	141	1	3	824	49	67
C168_FW_UT_2463	1804	6756	6.14	0.044	6.184	198	1	2	1152	40	65
C168_FW_UT_2468	1804	6754	5.66	0.434	6.094	157	1	3	13184	42	61
C168_FW_UT_2469	1804	6767	5.43	0.056	5.486	159	1	2	1792	38	51
C168_FW_UT_714	1804	6754	0.397	0.001	0.398	19	1	2	2	9	19
C202_FS_SZ_74	1556	5561	0.408	0.001	0.409	182	1	2	16	150	182
C202_FS_SZ_84	1556	5479	32.6	--		685	1	3	>1308604	233	237
C202_FW_SZ_100	1561	7484	3.78	0.007	3.787	117	1	3	267	27	67
C202_FW_SZ_103	1561	9024	115	--		919	1	5	>127632	262	264
C202_FW_SZ_61	1561	7490	12.3	0.01	12.31	214	1	4	314	21	52
C202_FW_SZ_77	1561	7611	0.826	0.002	0.828	185	1	2	64	156	185
C202_FW_SZ_87	1561	7696	101	--		1207	1	4	>85584	564	571
C202_FW_SZ_96	1561	7599	35.2	--		611	1	2	>43800	321	322
C202_FW_SZ_98	1561	7438	1.66	0.002	1.662	75	1	3	123	7	29
C202_FW_UT_2814	1820	9957	43.1	0.073	43.173	473	1	4	1198	27	77
C202_FW_UT_2815	1820	9957	43	0.074	43.074	473	1	4	1198	27	77
C208_FC_RZ_65	1513	4491	0.335	0.001	0.336	37	1	2	48	12	21
C208_FC_SZ_107	1513	4554	1.74	0.014	1.754	136	1	3	400	47	74
C210_FS_RZ_23	1608	4911	3.19	0.251	3.441	133	1	3	15406	32	51
C210_FS_SZ_103	1607	4915	1.9	--		145	1	3	>14213475	50	74
C210_FS_SZ_55	1608	4917	2.43	0.766	3.196	143	1	3	42608	41	67
C210_FS_SZ_78	1607	5071	1.17	0.004	1.174	225	1	3	48	173	185
C210_FW_RZ_30	1629	6407	8.03	1.16	9.19	173	1	3	58842	37	59
C210_FW_SZ_106	1628	6405	11.2	--		241	1	4	>4249594	64	86
C210_FW_SZ_128	1628	6401	1.03	0.582	1.612	84	1	2	28672	23	36
C210_FW_SZ_80	1628	6560	2.53	0.003	2.533	255	1	2	16	175	185
C210_FW_SZ_90	1628	6977	35.1	--		880	1	3	>37962	460	465
C210_FW_SZ_91	1628	6709	34.5	--		594	1	2	>2315168	320	328
C210_FW_UT_8630	1891	8511	15.8	0.299	16.099	161	1	3	16016	36	79
C210_FW_UT_8634	1891	8504	6.08	0.386	6.466	93	1	2	20480	27	53
C220_FV_SZ_39	1530	4788	12.6	--		784	1	3	>13548	633	633

Size Limit = 3

			Runtimes (sec)				PCS sizes			MUS sizes
Name	Vars	Clauses	PCSes	MUSes	Total	#PCSes	Min	Max	MUSes	Min	Max
C168_FW_SZ_107	1583	5939	124	--		1040	1	7	>14598284	104	128
C168_FW_SZ_128	1583	4777	7.32	--		335	1	4	>22838876	107	136
C168_FW_SZ_41	1583	4727	10.1	0.41	10.51	263	1	6	4500	26	62
C168_FW_SZ_66	1583	4751	13.1	18.4	31.5	499	1	7	434035	16	59
C168_FW_SZ_75	1583	4744	6.69	7.17	13.86	231	1	7	418463	48	74
C168_FW_UT_2463	1804	6756	38.1	--		1607	1	5	>836022	40	79
C168_FW_UT_2468	1804	6754	9.28	46.9	56.18	473	1	4	409509	36	73
C168_FW_UT_2469	1804	6767	30.9	483	513.9	1336	1	6	403392	35	66
C168_FW_UT_714	1804	6754	0.38	0	0.38	19	1	3	3	9	19
C202_FS_SZ_74	1556	5561	0.388	0.002	0.39	183	1	3	60	150	183
C202_FS_SZ_84	1556	5479	138	--		2147	1	7	>4067088	243	261
C202_FW_SZ_100	1561	7484	13.9	31.3	45.2	320	1	6	1105768	27	79
C202_FW_SZ_103	1561	9024	273	--		1234	1	10	>4181804	257	276
C202_FW_SZ_61	1561	7490	31.7	1.83	33.53	755	1	6	43238	19	69
C202_FW_SZ_77	1561	7611	0.727	0.003	0.73	187	1	3	144	156	187
C202_FW_SZ_87	1561	7696	--			>0
C202_FW_SZ_96	1561	7599	339	--		1810	1	5	>5610029	238	354
C202_FW_SZ_98	1561	7438	9.38	0.836	10.216	314	1	5	37718	7	43
C202_FW_UT_2814	1820	9957	267	125	392	2275	1	7	4869852	20	75
C202_FW_UT_2815	1820	9957	262	125	387	2275	1	7	4869852	20	75
C208_FC_RZ_65	1513	4491	1.12	0.041	1.161	77	1	3	2494	12	25
C208_FC_SZ_107	1513	4554	4.5	1.27	5.77	279	1	5	32718	44	82
C210_FS_RZ_23	1608	4911	3.59	10.9	14.49	195	1	5	474404	31	52
C210_FS_SZ_103	1607	4915	6.42	--		260	1	5	>15615479	54	78
C210_FS_SZ_55	1608	4917	4.93	388	392.93	246	1	8	14589828	41	77
C210_FS_SZ_78	1607	5071	1.35	0.032	1.382	267	1	5	432	170	194
C210_FW_RZ_30	1629	6407	10.8	--		266	1	6	>16859897	38	66
C210_FW_SZ_106	1628	6405	29.8	--		403	1	7	>18406484	59	91
C210_FW_SZ_128	1628	6401	2.66	19.9	22.56	197	1	5	493568	23	41
C210_FW_SZ_80	1628	6560	2.74	0.034	2.774	265	1	5	440	171	185
C210_FW_SZ_90	1628	6977	101	--		983	1	5	>1679408	414	423
C210_FW_SZ_91	1628	6709	112	--		1057	1	6	>2476166	470	486
C210_FW_UT_8630	1891	8511	65.7	259	324.7	985	1	7	4192496	34	69
C210_FW_UT_8634	1891	8504	68.9	167	235.9	760	1	6	5207976	26	84
C220_FV_SZ_39	1530	4788	30	--		1433	1	7	>2738674	281	305