SAT-Race 2006

SAT-Race
2006

Overview
Rules
Important Dates
Organizers
Downloads
Qualification
Solvers
Results
Result Analysis

Results

This page presents the results of SAT-Race 2006. Winner of SAT-Race is Minisat 2.0, Eureka achieved second place, and Rsat third place. The best student solver is MXC.

Summary

This table shows the number of instances solved by each solver (out of 100 instances in total; also split up into successfully processed SAT and UNSAT instances); the rank according to number of solved instances; number of speed-points assigned to solver (see Rules page for a description of speed-points); the rank according to speed-points; the total score; and the final ranking based on the total score.

	minisat 2.0	Eureka 2006	Rsat	Cadence MiniSat v1.14	Actin (minisat+i)	Barcelogic	PicoSAT	QPicoSAT	TINISAT	SAT4J	QCompSAT	zChaff 2006	CompSAT	MXC v.1^*	Mucsat	HyperSAT
#solved:	73	67	72	63	63	59	57	54	54	49	39	38	38	29	28	27
#solved SAT/UNSAT:	35/38	15/52	37/35	28/35	29/34	23/36	24/33	18/36	21/33	21/28	12/27	10/28	17/21	12/17	10/18	10/17
rank by solved:	1	3	2	4	4	6	7	8	8	10	11	12	12	14	15	16
speed-points:	9.71	13.87	8.45	6.39	6.29	5.98	5.00	5.39	4.91	4.20	3.22	3.78	3.21	2.23	2.09	2.99
rank by speed:	2	1	3	4	5	6	8	7	9	10	12	11	13	15	16	14
total score:	82.71	80.87	80.45	69.39	69.29	64.98	62.00	59.39	58.91	53.20	42.22	41.78	41.21	31.23	30.09	29.99
rank:	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16

^*Important note: Due to an error in our execution environment in combination with MXC v.1, this solver was restricted to use only 128 MB of main memory. With 1.5 GB of main memory, MXC v.1 can solve 41 instances, and should thus be considered on place 11, instead of 14, in the ranking.

Benchmark Suite Summary

In this table you can find a summary of instances solved by each solver, grouped by benchmark suites. We had five benchmark suites in SAT-Race:

IBM: instances from Bounded Model Checking (BMC)
Manolios: instances from pipelined machine verification
Mixed: instances from former SAT-Competitions
Mironov-Zhang: instances from cryptanalysis
Velev: instances from pipelined machine verification

Best results in each group are indicated by bold numbers.

	minisat 2.0	Eureka 2006	Rsat	Cadence MiniSat v1.14	Actin (minisat+i)	Barcelogic	PicoSAT	QPicoSAT	TINISAT	SAT4J	QCompSAT	zChaff 2006	CompSAT	MXC v.1	Mucsat	HyperSAT
IBM (20 inst.)	19	16	19	16	16	16	16	18	13	14	12	9	12	9	10	9
Manolios (20 inst.)	14	20	12	12	12	11	11	12	9	8	11	10	7	4	7	5
Mixed (30 inst.)	20	17	22	20	17	18	14	14	14	14	8	10	7	9	7	8
Mironov-Zhang (10 inst.)	9	0	8	7	8	0	4	5	2	5	5	0	2	4	2	2
Velev (20 inst.)	11	14	11	8	10	14	12	5	16	8	3	9	10	3	2	3
total #solved:	73	67	72	63	63	59	57	54	54	49	39	38	38	29	28	27

Detailed Results

This table contains run-times for all solvers on all instances (you can download the whole set of instances from the Downloads page).

Instance	SAT/ UNSAT	minisat 2.0	Eureka 2006	Rsat	Cadence MiniSat v1.14	Actin (minisat+i)	Barcelogic	PicoSAT	QPicoSAT	TINISAT	SAT4J	QCompSAT	zChaff 2006	CompSAT	MXC v.1	Mucsat	HyperSAT
IBM Benchmark Suite (10 SAT / 10 UNSAT)
ibm-2002-05r-k90.cnf	SAT	13.67	37.93	40.84	28.66	73.41	88.86	200.41	22.65	579.87	101.44	-----	-----	366.96	-----	48.50	-----
ibm-2002-07r-k100.cnf	UNSAT	6.08	1.69	19.18	-----	8.08	5.25	6.19	2.18	10.84	15.21	1.55	6.03	53.84	59.89	-----	-----
ibm-2002-11r1-k45.cnf	SAT	73.48	272.44	194.54	174.10	166.53	426.60	665.98	51.99	-----	-----	210.83	-----	-----	-----	-----	-----
ibm-2002-19r-k100.cnf	SAT	164.71	-----	360.09	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
ibm-2002-21r-k95.cnf	SAT	251.49	-----	295.73	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
ibm-2002-26r-k45.cnf	UNSAT	42.64	64.52	1.56	4.74	-----	1.43	2.38	42.19	6.50	3.69	17.51	-----	3.07	-----	24.29	3.34
ibm-2002-27r-k95.cnf	SAT	19.02	42.43	28.38	42.32	52.76	85.44	46.71	16.03	231.29	95.33	55.25	342.32	121.45	227.31	-----	80.77
ibm-2004-03-k70.cnf	SAT	22.33	71.00	27.73	59.38	114.93	99.57	56.81	41.34	195.54	111.94	-----	-----	385.91	81.70	-----	-----
ibm-2004-04-k100.cnf	SAT	124.65	282.43	849.59	469.20	512.75	793.95	321.15	162.54	-----	-----	-----	-----	-----	-----	644.58	-----
ibm-2004-06-k90.cnf	SAT	29.07	335.76	47.60	191.22	112.33	240.90	208.54	161.97	-----	323.88	432.12	-----	-----	-----	-----	-----
ibm-2004-19-k90.cnf	SAT	83.81	-----	196.96	132.67	480.79	-----	-----	702.11	-----	-----	-----	-----	-----	-----	-----	-----
ibm-2004-1_11-k25.cnf	UNSAT	4.95	10.27	9.10	9.71	6.84	8.06	14.51	6.35	25.79	37.39	16.63	44.09	97.21	17.73	211.70	214.16
ibm-2004-1_31_2-k25.cnf	UNSAT	79.20	52.26	210.28	95.15	254.54	684.67	663.40	46.51	579.33	476.91	-----	-----	-----	-----	-----	476.95
ibm-2004-26-k25.cnf	UNSAT	55.20	22.78	19.13	9.05	41.43	28.08	1.23	7.37	2.59	2.66	265.43	2.71	67.23	-----	5.55	1.79
ibm-2004-2_02_1-k100.cnf	UNSAT	10.57	30.96	27.06	18.57	12.88	47.04	16.33	6.50	104.27	98.66	12.77	211.95	24.92	222.30	66.83	117.79
ibm-2004-2_14-k45.cnf	UNSAT	16.86	28.84	27.63	24.84	25.86	52.83	45.59	12.62	131.33	158.55	90.88	185.27	107.75	115.23	723.98	-----
ibm-2004-3_02_1-k95.cnf	UNSAT	7.85	5.57	2.78	2.08	6.51	2.38	4.41	2.78	1.87	32.48	3.97	26.98	1.29	2.29	10.30	378.15
ibm-2004-3_02_3-k95.cnf	SAT	13.55	29.38	17.40	8.02	8.42	18.41	9.04	6.16	0.57	48.43	5.10	1.05	107.02	19.47	20.07	45.45
ibm-2004-3_11-k60.cnf	UNSAT	-----	-----	-----	-----	-----	-----	-----	637.61	-----	-----	-----	-----	-----	-----	-----	-----
ibm-2004-6_02_3-k100.cnf	UNSAT	5.53	29.46	16.21	14.37	3.50	7.28	12.13	5.19	8.21	33.99	155.41	5.67	330.58	10.58	219.34	218.16
Manolios Benchmark Suite (20 UNSAT)
manol-pipe-c10id_s.cnf	UNSAT	9.52	18.27	14.31	5.71	6.09	23.31	7.16	12.20	84.99	44.86	367.30	91.52	21.68	-----	172.48	18.21
manol-pipe-c10nidw_s.cnf	UNSAT	318.93	687.83	142.53	331.14	-----	-----	147.38	75.72	-----	-----	-----	-----	76.78	-----	-----	765.39
manol-pipe-c6nidw_i.cnf	UNSAT	216.35	271.21	-----	665.26	558.10	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
manol-pipe-c7b.cnf	UNSAT	42.16	27.26	68.29	53.64	53.80	53.68	73.68	32.70	188.32	159.02	85.71	121.23	-----	-----	750.00	-----
manol-pipe-c7b_i.cnf	UNSAT	41.99	24.55	91.65	64.76	40.67	57.43	89.46	65.04	192.96	125.98	64.62	112.50	-----	-----	607.16	-----
manol-pipe-c7bidw_i.cnf	UNSAT	550.63	654.39	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
manol-pipe-c7nidw.cnf	UNSAT	603.79	688.49	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
manol-pipe-c9.cnf	UNSAT	14.95	3.24	19.49	21.71	13.76	8.55	15.85	10.46	32.94	28.88	8.26	8.75	213.52	393.37	33.95	-----
manol-pipe-c9nidw_s.cnf	UNSAT	292.42	482.86	198.24	295.14	759.41	140.10	145.88	60.74	-----	665.37	-----	-----	53.53	-----	342.36	-----
manol-pipe-f10ni.cnf	UNSAT	-----	427.67	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
manol-pipe-f6bi.cnf	UNSAT	6.78	5.31	9.84	8.89	6.63	12.98	10.05	5.69	12.85	44.71	16.33	14.99	49.07	6.11	50.41	196.20
manol-pipe-f7idw.cnf	UNSAT	-----	82.44	589.94	-----	-----	552.07	-----	411.66	625.50	-----	-----	669.36	-----	-----	-----	-----
manol-pipe-f9b.cnf	UNSAT	-----	144.10	-----	-----	-----	-----	-----	-----	-----	-----	541.68	-----	-----	-----	-----	-----
manol-pipe-f9n.cnf	UNSAT	-----	148.91	-----	-----	-----	-----	-----	-----	-----	-----	581.63	-----	-----	-----	-----	-----
manol-pipe-g10b.cnf	UNSAT	226.04	65.30	331.81	133.46	352.21	256.85	376.21	314.28	-----	-----	359.93	619.63	-----	-----	-----	-----
manol-pipe-g10bidw.cnf	UNSAT	-----	417.62	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
manol-pipe-g10id.cnf	UNSAT	183.04	63.55	150.16	152.29	97.50	128.61	300.85	269.69	391.67	-----	270.20	297.06	-----	-----	-----	-----
manol-pipe-g10nid.cnf	UNSAT	-----	341.53	-----	-----	810.14	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
manol-pipe-g6bi.cnf	UNSAT	3.37	2.23	2.46	2.41	1.66	2.27	2.47	1.92	4.39	10.45	3.92	4.37	6.71	3.71	19.28	235.13
manol-pipe-g7nidw.cnf	UNSAT	42.11	13.93	33.29	28.51	25.42	58.41	74.85	54.12	50.41	139.75	57.45	83.93	168.50	93.01	-----	224.08
Mixed Benchmark Suite (13 SAT / 17 UNSAT)
aloul-chnl11-13.cnf	UNSAT	-----	234.87	321.55	889.20	-----	-----	-----	-----	-----	-----	-----	128.99	-----	-----	-----	-----
een-pico-prop01-75.cnf	UNSAT	2.78	6.01	3.10	4.07	5.29	2.96	5.26	4.04	42.26	16.87	7.49	86.82	39.04	10.70	90.22	20.71
een-pico-prop05-50.cnf	UNSAT	43.34	41.76	97.88	134.80	89.94	66.94	257.57	29.45	756.48	303.55	-----	-----	-----	-----	-----	-----
een-tip-sat-nusmv-t5.B.cnf	SAT	2.27	3.34	15.44	14.40	6.98	13.36	11.68	4.17	11.37	29.49	7.18	14.02	81.51	54.08	12.80	4.60
een-tip-sat-nusmv-tt5.B.cnf	SAT	1.98	3.47	12.35	15.76	6.78	14.37	12.51	3.89	12.27	30.07	8.25	12.75	76.68	81.75	19.56	3.78
een-tip-uns-nusmv-t5.B.cnf	UNSAT	1.82	3.34	8.04	9.61	3.06	7.75	5.13	3.05	3.47	10.45	3.62	4.24	75.78	66.52	9.07	4.28
goldb-heqc-alu4mul.cnf	UNSAT	733.07	-----	548.01	459.87	599.29	690.65	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
goldb-heqc-dalumul.cnf	UNSAT	-----	502.34	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
goldb-heqc-desmul.cnf	UNSAT	72.39	80.02	80.09	57.25	63.73	112.35	82.18	78.37	89.96	147.69	364.04	128.52	295.38	121.58	-----	-----
goldb-heqc-frg2mul.cnf	UNSAT	402.51	99.48	593.23	329.18	285.66	256.38	635.61	846.49	-----	-----	-----	623.98	-----	-----	799.36	-----
goldb-heqc-i10mul.cnf	UNSAT	-----	599.01	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
goldb-heqc-i8mul.cnf	UNSAT	685.19	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
goldb-heqc-term1mul.cnf	UNSAT	-----	54.86	-----	-----	-----	404.19	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
grieu-vmpc-s05-25.cnf	SAT	565.18	-----	125.18	368.65	382.50	124.58	834.28	41.21	402.26	-----	-----	-----	410.37	464.25	-----	36.33
grieu-vmpc-s05-27.cnf	SAT	-----	-----	112.26	597.67	-----	858.05	-----	-----	-----	334.55	-----	94.57	-----	-----	-----	550.66
grieu-vmpc-s05-28.cnf	SAT	-----	-----	89.16	-----	-----	625.38	209.26	-----	89.36	-----	-----	-----	-----	894.91	29.53	191.75
grieu-vmpc-s05-34.cnf	SAT	-----	-----	751.30	-----	-----	-----	-----	-----	-----	-----	-----	305.47	-----	-----	-----	-----
hoons-vbmc-lucky7.cnf	UNSAT	47.08	8.68	82.48	39.93	50.23	8.74	14.01	69.43	300.95	116.70	202.71	-----	-----	44.46	-----	-----
maris-s03-gripper11.cnf	SAT	-----	-----	422.36	-----	-----	-----	301.15	-----	-----	-----	-----	-----	-----	-----	-----	-----
narain-vpn-clauses-6.cnf	SAT	793.98	-----	275.26	668.03	508.64	-----	-----	-----	563.51	741.85	-----	-----	-----	-----	-----	-----
schup-l2s-guid-1-k56.cnf	UNSAT	769.56	-----	-----	542.29	787.74	-----	-----	444.22	-----	-----	-----	-----	-----	-----	-----	-----
schup-l2s-motst-2-k315.cnf	SAT	86.24	225.03	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
simon-s02-w08-18.cnf	SAT	126.91	312.46	147.69	246.45	354.54	535.17	527.24	235.57	-----	586.26	-----	-----	-----	-----	-----	-----
simon-s02b-dp11u10.cnf	UNSAT	234.37	-----	450.19	215.55	191.46	-----	-----	-----	801.86	631.43	-----	-----	-----	-----	-----	-----
simon-s02b-k2f-gr-rcs-w8.cnf	UNSAT	-----	213.09	-----	-----	-----	265.13	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
simon-s02b-r4b1k1.1.cnf	SAT	737.78	-----	141.92	104.46	-----	-----	-----	-----	-----	182.37	-----	-----	-----	-----	-----	-----
simon-s03-fifo8-300.cnf	UNSAT	35.56	212.13	362.70	157.18	275.33	243.67	219.81	40.24	254.20	310.78	306.37	-----	-----	-----	-----	-----
simon-s03-fifo8-400.cnf	UNSAT	118.28	258.48	677.61	325.55	504.17	578.55	-----	122.45	687.26	-----	-----	-----	-----	-----	-----	-----
vange-col-abb313GPIA-9-c.cnf	SAT	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	204.39
vange-col-inithx.i.1-cn-54.cnf	SAT	12.07	-----	14.53	14.34	5.56	4.13	19.91	24.32	464.10	29.53	661.76	214.34	84.68	214.59	21.68	-----
Mironov-Zhang Benchmark Suite (10 SAT)
mizh-md5-47-3.cnf	SAT	541.72	-----	516.99	243.50	318.49	-----	-----	235.07	-----	-----	312.02	-----	-----	869.45	-----	-----
mizh-md5-47-4.cnf	SAT	-----	-----	471.34	326.93	-----	-----	298.53	269.68	-----	738.51	706.62	-----	-----	-----	-----	-----
mizh-md5-47-5.cnf	SAT	628.56	-----	200.90	-----	539.19	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	753.51
mizh-md5-48-2.cnf	SAT	454.05	-----	-----	-----	255.08	-----	-----	-----	-----	-----	-----	-----	-----	528.63	-----	-----
mizh-md5-48-5.cnf	SAT	287.32	-----	-----	427.04	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	650.80
mizh-sha0-35-2.cnf	SAT	277.52	-----	407.36	309.31	747.17	-----	-----	760.77	-----	187.57	686.17	-----	-----	-----	-----	-----
mizh-sha0-35-3.cnf	SAT	30.48	-----	245.96	746.00	306.71	-----	455.07	146.89	628.43	586.62	371.21	-----	541.51	-----	376.75	-----
mizh-sha0-35-4.cnf	SAT	214.70	-----	108.33	-----	226.39	-----	546.67	774.56	-----	409.73	-----	-----	385.35	222.54	-----	-----
mizh-sha0-35-5.cnf	SAT	140.18	-----	247.98	234.61	275.83	-----	666.83	-----	355.79	621.89	676.79	-----	-----	168.62	502.77	-----
mizh-sha0-36-2.cnf	SAT	282.88	-----	449.50	771.04	521.15	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
Velev Benchmark Suite (10 SAT / 10 UNSAT)
velev-engi-uns-1.0-4nd.cnf	UNSAT	76.90	80.49	59.92	51.86	47.34	44.10	181.41	118.63	77.80	95.63	645.17	452.09	507.57	384.01	-----	90.62
velev-engi-uns-1.0-5c1.cnf	UNSAT	11.24	8.59	8.32	5.66	5.88	8.07	17.72	15.73	7.12	17.92	46.04	12.33	27.69	18.16	52.22	16.08
velev-fvp-sat-3.0-b18.cnf	SAT	-----	-----	269.14	-----	-----	302.90	392.33	-----	777.43	-----	-----	513.46	377.19	-----	86.84	-----
velev-live-uns-2.0-ebuf.cnf	UNSAT	49.92	23.15	60.79	58.90	35.17	70.14	71.34	42.00	35.71	66.15	318.96	63.07	589.54	96.77	-----	162.13
velev-npe-1.0-9dlx-b71.cnf	SAT	818.86	-----	845.91	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
velev-pipe-o-uns-1.0-7.cnf	UNSAT	-----	310.31	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
velev-pipe-o-uns-1.1-6.cnf	UNSAT	-----	47.09	-----	-----	-----	659.56	109.01	147.61	100.32	-----	-----	113.65	-----	-----	-----	-----
velev-pipe-sat-1.0-b10.cnf	SAT	15.83	133.86	-----	-----	40.31	35.80	307.74	-----	21.75	-----	-----	-----	222.34	-----	-----	-----
velev-pipe-sat-1.0-b7.cnf	SAT	-----	213.18	84.46	40.11	57.43	247.48	-----	-----	21.23	-----	-----	-----	-----	-----	-----	-----
velev-pipe-sat-1.0-b9.cnf	SAT	39.85	329.45	-----	-----	49.99	12.90	-----	-----	750.93	-----	-----	-----	76.17	-----	-----	-----
velev-pipe-sat-1.1-b7.cnf	SAT	31.97	-----	384.00	-----	-----	122.18	696.85	-----	384.62	-----	-----	-----	-----	-----	-----	-----
velev-pipe-uns-1.0-8.cnf	UNSAT	-----	183.34	-----	-----	-----	-----	-----	-----	543.96	-----	-----	819.51	-----	-----	-----	-----
velev-pipe-uns-1.0-9.cnf	UNSAT	-----	166.06	-----	-----	-----	-----	883.01	664.43	134.71	446.49	-----	-----	-----	-----	-----	-----
velev-pipe-uns-1.1-7.cnf	UNSAT	-----	66.25	-----	-----	-----	752.68	652.44	-----	117.61	-----	-----	184.23	-----	-----	-----	-----
velev-vliw-sat-2.0-b6.cnf	SAT	144.23	154.21	88.03	60.13	27.74	33.20	173.14	-----	45.45	44.81	-----	55.04	13.23	-----	-----	-----
velev-vliw-sat-4.0-b1.cnf	SAT	65.18	-----	106.50	69.22	61.90	114.32	-----	-----	153.86	160.66	-----	-----	236.55	-----	-----	-----
velev-vliw-sat-4.0-b3.cnf	SAT	86.87	-----	41.78	59.71	69.53	125.91	660.48	-----	97.58	201.12	-----	54.78	88.78	-----	-----	-----
velev-vliw-sat-4.0-b4.cnf	SAT	147.37	-----	318.37	85.97	71.61	272.96	532.35	-----	136.55	187.84	-----	-----	360.74	-----	-----	-----
velev-vliw-uns-2.0-iq4.cnf	UNSAT	-----	500.85	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
velev-vliw-uns-4.0-9C1.cnf	UNSAT	-----	341.77	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----	-----
#solved:		73	67	72	63	63	59	57	54	54	49	39	38	38	29	28	27
#solved SAT/UNSAT:		35/38	15/52	37/35	28/35	29/34	23/36	24/33	18/36	21/33	21/28	12/27	10/28	17/21	12/17	10/18	10/17
rank by solved:		1	3	2	4	4	6	7	8	8	10	11	12	12	14	15	16
speed-points:		9.71	13.87	8.45	6.39	6.29	5.98	5.00	5.39	4.91	4.20	3.22	3.78	3.21	2.23	2.09	2.99
rank by speed:		2	1	3	4	5	6	8	7	9	10	12	11	13	15	16	14
total score:		82.71	80.87	80.45	69.39	69.29	64.98	62.00	59.39	58.91	53.20	42.22	41.78	41.21	31.23	30.09	29.99
rank:		1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16

Further Solvers

This table contains run-times of further solvers on the SAT-Race instances.

SatELite GTI: First place SAT-Competition 2005, industrial category SAT+UNSAT
minisat 1.13: Second place SAT-Competition 2005, industrial category SAT+UNSAT
HaifaSAT: Shared third place SAT-Competition 2005, industrial category SAT+UNSAT
Siege v4: Third place, first round SAT-Competition 2003, industrial cat., SAT+UNSAT
zChaff rand: Second place SAT-Competition 2005, industrial category UNSAT
BerkMin 561: Second place SAT-Competition 2003, industrial category SAT+UNSAT