Qute_opt500 results solving families

Qute_opt500 results solving families - 2017

Family	# Total	# Sat	# Unsat	Time
Abduction	26	0	1	20892.45
Adder	114	0	0	102600
amba	22	0	1	18063.76
arithmetic	22	3	0	9000.81
blackbox-01X-QBF	133	0	8	71864.63
BMC	98	3	2	51645.87
C432	21	0	0	18900
C499	31	0	1	20698.47
C5315	57	1	1	31917.44
C6288	76	1	0	60313.32
C880	60	0	1	44436.93
circuits	84	1	0	68511.6
conformant_planning	60	1	3	41276.5
Connect2	1	1	0	436.36
Connect3	2	0	0	1800
Connect4	43	0	1	37800.07
Connect5	2	0	1	900.57
Connect6	3	0	1	1800.08
Connect7	4	0	0	3600
Connect8	2	0	2	0.47
Counter	22	2	0	14506.97
cycle-sched	24	0	0	21600
Debug	125	5	0	86166.96
disjunctive_decomposition	23	1	1	11732.6
driver	18	2	2	30.2
dungeon	115	1	25	2755.56
evader-pursuer-4x4-logarithmic	10	0	0	9000
evader-pursuer-4x4-standard	65	7	0	863.83
evader-pursuer-6x6-logarithmic	50	0	2	43062.65
evader-pursuer-6x6-standard	77	0	0	69300
evader-pursuer-8x8-logarithmic	51	0	0	45900
formula_add	39	3	0	31607.99
fpu	20	0	20	44.66
genbuf	22	0	0	19800
Generalized-Tic-Tac-Toe	32	0	3	23071.12
genpatch	20	0	0	18000
HardwareFixpoint	125	2	13	40601.51
hwmcc	16	1	2	6261.24
hyperLTL	4	1	1	0.04
incrementer-encoder	55	1	9	27106.98
irqlkeapclte	121	0	0	108900
ISCAS89	7	2	2	17.18
ITC99	57	3	1	36959.98
jmc_quant	6	0	0	5400
jmc_quant_squaring	98	1	0	84050.4
k_branch_n	56	6	0	8845.92
k_branch_p	85	0	8	9525.05
k_ph_p	80	0	0	72000
LinearBitvectorRankingFunction	119	5	0	85293.99
ltl2aig-comp	19	0	1	10845.15
LTL2DBA	9	0	1	6300.12
LTL2DPA	10	0	1	6300.99
mqm	34	0	0	30600
mult-matrix	24	0	0	21600
Planning-CTE	131	2	27	14404.34
QBF-Hardness	60	0	4	40522.68
qbfeval12	7	2	0	1917.2
RankingFunctions	2	2	0	2.82
Reduction-finding	45	0	1	37036.64
s1196	15	0	0	13500
s1269	17	0	0	15300
s298	14	1	0	6680.31
s3330	21	0	0	18900
s499	13	0	0	11700
s510	9	0	0	8100
s641	16	1	1	1729.6
s713	15	0	1	6070.32
s820	15	0	0	13500
sketch	16	0	0	14400
Sorting_networks	81	1	1	56963.9
SzymanskiP	25	0	2	2814.39
terminator	78	1	8	728.73
tipdiam	85	4	0	47730.98
tipfixpoint	93	7	0	30421.15
toy	14	2	2	9.08
trafficlight-controller	10	0	10	44.69
uclid	30	0	0	27000

QBF Solver Evaluation Portal

QBFEVALs

QBF GALLERIES

DOWNLOADS

qbflib.org

Qute_opt500 results solving families - 2017