mpiDepQBF results solving families

mpiDepQBF results solving families - 2016

Family	# Total	# Sat	# Unsat	Time
Abduction	71	4	5	6139.45
Adder	115		2	60600.76
blackbox-01X-QBF	77		7	18154.5
blackbox_design	76	2		40008.68
Blocks	88	3	6	6812.31
BMC	91			54600
bomb	51	4	1	15656.27
C432	73	3	4	9376.59
C499	76	3	2	21357.41
C5315	86	2	1	34680.47
C6288	86	1		45601
C880	78	2		36002.32
Chain	82	7		23737.9
circuits	75	1		41400.6
conformant_planning	79	5	2	17569.29
Connect4	68		6	19410.33
Counter	54	6		14445.09
Debug	103			61800
DFlipFlop	73		10	124.3
dungeon	73		4	30925.84
evader-pursuer-4x4-logarithmic	61	7		4663.06
evader-pursuer-4x4-standard	65	7		297.09
evader-pursuer-6x6-logarithmic	74		6	17279.46
evader-pursuer-6x6-standard	77			46200
evader-pursuer-8x8-logarithmic	78		5	25945.99
FPGA_PLB_FIT_FAST	38	4	1	3.58
FPGA_PLB_FIT_SLOW	25		2	4709.94
fpu	47		3	20857.39
Generalized-Tic-Tac-Toe	54	1	8	5491.18
HardwareFixpoint	81			48600
Impl	74	10		193.27
incrementer-encoder	67		6	24637.78
irqlkeapclte	121			72600
ISCAS89	32	6	1	35.11
ITC99	56	2	1	22213.66
jmc_quant_squaring	118	2	2	47142.33
k_branch_n	88	3		40250.82
k_branch_p	103	1		58466.88
k_d4_n	73	3		33602.43
k_d4_p	72		10	5.28
k_dum_n	66	5		24505.36
k_dum_p	74		7	15448.8
k_grz_n	68	10		2642.9
k_grz_p	70	6	4	1520.51
k_lin_n	64	10		342.98
k_lin_p	65	1	9	26.05
k_path_n	67	9		4338.07
k_path_p	67	6	2	9624.84
k_ph_n	74	10		257.88
k_ph_p	85	5	3	14103.01
k_poly_n	68	1		37200.54
k_poly_p	64		10	4.14
k_t4p_n	71	1		38428.56
k_t4p_p	76		1	39243.98
LinearBitvectorRankingFunction	86			51600
Logn	29		2	6053.36
mqm	84	5	5	620.65
MutexP	78	3		28817.3
Planning-CTE	55	2		27603.53
QBF-Hardness	63		8	11155.57
qbfeval12	27	2	4	448.08
Qshifter	62	3		21001.54
RankingFunctions	61	5		19202.2
Reduction-finding	65	1	5	22831.08
Rewriting	45		5	14552.99
s1196	44			26400
s1269	76			45600
s27	36	1	3	4.02
s298	70	1		36600.63
s3330	76			45600
s386	69			41400
s499	62			37200
s510	59			35400
s641	55			33000
s713	73			43800
s820	72			43200
Sorting_networks	110	4	1	42501.36
SzymanskiP	99		2	49294.63
term1	69	4	4	52.09
terminator	86		9	9910.75
tipdiam	86	5		30604.94
tipfixpoint	81	3	3	23563.04
ToiletA	48		1	25200.42
ToiletC	48	1	1	22200.61
ToiletG	43			25800
trafficlight-controller	45		9	4804.69
Tree	74	2	8	4.08
uclid	30			18000
VonNeumann	75		5	23464.9
wmiforward	74	4		28239.92
z4ml	61	4	4	3.12

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

mpiDepQBF results solving families - 2016