QF_IDL (Single Query Track)

Competition results for the QF_IDL logic in the Single Query Track.

Page generated on 2023-07-06 16:04:54 +0000

Benchmarks: 1203
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Z3++	Z3++	Z3++	Z3++	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Z3++	0	1041	59582.736	59480.869	1041	670	371	162	162	0
2019-Par4n	0	981	55994.444	14238.832	981	637	344	222	222	0
Yices2	0	963	29563.41	29536.133	963	634	329	240	240	0
cvc5	0	902	79040.08	78959.624	902	544	358	301	301	0
OpenSMT	0	880	70196.998	70099.563	880	572	308	323	323	0
SMTInterpol	0	687	88913.525	73732.003	687	418	269	516	516	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Z3++	0	1041	59582.736	59480.869	1041	670	371	162	162	0
2019-Par4n	0	1032	176133.254	44573.55	1032	664	368	171	171	0
Yices2	0	963	29563.41	29536.133	963	634	329	240	240	0
cvc5	0	902	79040.08	78959.624	902	544	358	301	301	0
OpenSMT	0	880	70196.998	70099.563	880	572	308	323	323	0
SMTInterpol	0	689	91542.965	75915.406	689	419	270	514	514	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Z3++	0	670	44452.369	44366.335	670	670	0	56	477	162	0
2019-Par4n	0	664	98908.089	25051.757	664	664	0	62	477	171	0
Yices2	0	634	19202.321	19173.926	634	634	0	92	477	240	0
OpenSMT	0	572	58134.023	58035.533	572	572	0	154	477	323	0
cvc5	0	544	55228.192	55152.586	544	544	0	182	477	301	0
SMTInterpol	0	419	62884.841	56789.379	419	419	0	307	477	514	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Z3++	0	371	15130.367	15114.534	371	0	371	37	795	162	0
2019-Par4n	0	368	77225.165	19521.792	368	0	368	40	795	171	0
cvc5	0	358	23811.888	23807.037	358	0	358	50	795	301	0
Yices2	0	329	10361.088	10362.206	329	0	329	79	795	240	0
OpenSMT	0	308	12062.975	12064.03	308	0	308	100	795	323	0
SMTInterpol	0	270	28658.124	19126.027	270	0	270	138	795	514	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Par4n	0	856	4934.21	1336.47	856	566	290	347	347	0
Yices2	0	852	1474.867	1445.117	852	565	287	351	351	0
Z3++	0	785	2310.273	2277.72	785	507	278	418	418	0
OpenSMT	0	579	2069.908	2045.2	579	318	261	624	624	0
cvc5	0	578	2383.203	2364.092	578	304	274	625	625	0
SMTInterpol	0	403	4610.526	1984.176	403	221	182	800	800	0

n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.