aqua-s2v results solving families

aqua-s2v results solving families - 2016

Family	# Total	# Sat	# Unsat	Time
Abduction	71	3	5	11107.72
Adder	115		2	60587.98
blackbox-01X-QBF	77		7	18041.48
blackbox_design	76	10		9.3
Blocks	88	3	7	4748.61
BMC	91	3	2	32639.54
bomb	51	3		22778.69
C432	73	3	3	14299.89
C499	76	3	1	25810.86
C5315	86	2	1	34446.14
C6288	86	2		40193.96
C880	78	2	1	30606.48
Chain	82	10		2.5
circuits	75	1		41390.73
conformant_planning	79	4	2	24747.07
Connect4	68		6	9951.31
Counter	54	7		13381.05
Debug	103			61800
DFlipFlop	73		10	102.42
dungeon	73		1	42373.64
evader-pursuer-4x4-logarithmic	61	6		7141.46
evader-pursuer-4x4-standard	65			38985.1
evader-pursuer-6x6-logarithmic	74		5	12517.5
evader-pursuer-6x6-standard	77			46195.86
evader-pursuer-8x8-logarithmic	78		5	21561.7
FPGA_PLB_FIT_FAST	38	4	1	3.68
FPGA_PLB_FIT_SLOW	25	1	2	1152.94
fpu	47		10	671.16
Generalized-Tic-Tac-Toe	54	1	5	7532.51
HardwareFixpoint	81	2	2	35062.92
Impl	74	10		0
incrementer-encoder	67	1	6	19182.81
irqlkeapclte	121			72568.17
ISCAS89	32	4	1	2282.73
ITC99	56	1	1	19467.88
jmc_quant_squaring	118	1	1	57811.97
k_branch_n	88	3		27343.96
k_branch_p	103		1	36514.4
k_d4_n	73	3		33596.21
k_d4_p	72		10	2.01
k_dum_n	66	6		19456.4
k_dum_p	74		8	11311.18
k_grz_n	68	7		15007.54
k_grz_p	70		8	7722.1
k_lin_n	64	10		43.3
k_lin_p	65		10	2.76
k_path_n	67	4		24610
k_path_p	67		2	32385.69
k_ph_n	74	10		411.48
k_ph_p	85		3	40185.97
k_poly_n	68	10		1.57
k_poly_p	64		10	1.03
k_t4p_n	71	1		38398.86
k_t4p_p	76		1	39016.62
LinearBitvectorRankingFunction	86			51576.36
Logn	29		4	43
mqm	84	3	5	16387.31
MutexP	78	7		3.96
Planning-CTE	55	2	1	24887.68
QBF-Hardness	63		6	22034.14
qbfeval12	27	1	4	2999.44
Qshifter	62	5		7549.83
RankingFunctions	61	10		10.93
Reduction-finding	65	2	5	21985.14
Rewriting	45		10	27.11
s1196	44	1		21647.42
s1269	76			45600
s27	36	1	3	0.4
s298	70	2		31992.52
s3330	76	1		40881.2
s386	69	1	2	30708.08
s499	62	1		36683.7
s510	59	1		32318.04
s641	55	4	1	17359.95
s713	73	5		21507.76
s820	72	4		29418.45
Sorting_networks	110	2	3	37547.73
SzymanskiP	99		10	2057.1
term1	69	4	4	402.06
terminator	86		9	6666.49
tipdiam	86	4		37187.96
tipfixpoint	81	3	3	25820.78
ToiletA	48	3	7	46.95
ToiletC	48	1	8	3000.16
ToiletG	43	7		0.07
trafficlight-controller	45		8	5083.29
Tree	74	2	8	0
uclid	30			17994.82
VonNeumann	75		10	525.03
wmiforward	74	7		15618.15
z4ml	61	4	4	0.07

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

aqua-s2v results solving families - 2016