QF_UFIDL (Single Query Track)

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

Page generated on 2022-08-10 11:17:45 +0000

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Yices2	Yices2	smtinterpol	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	260	65072.582	65065.242	260	70	190	40	40	0
2021-SMTInterpoln	0	251	80383.389	76302.061	251	83	168	49	49	0
Yices2	0	246	81761.584	81770.967	246	56	190	54	54	0
cvc5	0	241	107660.254	107677.18	241	70	171	59	59	0
smtinterpol	0	239	94275.371	87469.205	239	83	156	61	61	0
MathSATn	0	227	106349.727	106306.295	227	38	189	73	73	0
veriT	0	225	98856.176	98866.326	225	73	152	75	72	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	260	65076.302	65063.602	260	70	190	40	40	0
2021-SMTInterpoln	0	257	80821.679	75397.541	257	83	174	43	43	0
Yices2	0	246	81767.614	81769.267	246	56	190	54	54	0
smtinterpol	0	242	94887.621	86253.554	242	83	159	58	58	0
cvc5	0	241	107669.854	107674.76	241	70	171	59	59	0
MathSATn	0	227	106364.457	106302.945	227	38	189	73	73	0
veriT	0	225	98863.836	98863.796	225	73	152	75	72	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2021-SMTInterpoln	0	83	7851.837	7175.134	83	83	0	2	215	43	0
smtinterpol	0	83	7976.889	7224.821	83	83	0	2	215	58	0
veriT	0	73	18941.707	18941.043	73	73	0	12	215	72	0
z3-4.8.17n	0	70	19444.274	19443.365	70	70	0	15	215	40	0
cvc5	0	70	31063.117	31065.364	70	70	0	15	215	59	0
Yices2	0	56	40686.234	40686.988	56	56	0	29	215	54	0
MathSATn	0	38	56438.438	56435.266	38	38	0	47	215	73	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Yices2	0	190	41081.381	41082.279	190	0	190	25	85	54	0
z3-4.8.17n	0	190	45632.028	45620.237	190	0	190	25	85	40	0
MathSATn	0	189	49926.019	49867.679	189	0	189	26	85	73	0
2021-SMTInterpoln	0	174	72969.842	68222.407	174	0	174	41	85	43	0
cvc5	0	171	76606.736	76609.396	171	0	171	44	85	59	0
smtinterpol	0	159	86910.732	79028.732	159	0	159	56	85	58	0
veriT	0	152	79922.13	79922.752	152	0	152	63	85	72	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-4.8.17n	0	222	2214.939	2200.243	222	66	156	78	78	0
Yices2	0	199	2584.897	2584.997	199	39	160	101	101	0
veriT	0	198	2854.967	2853.887	198	63	135	102	102	0
2021-SMTInterpoln	0	189	5311.607	3824.831	189	62	127	111	111	0
smtinterpol	0	181	5560.887	4052.382	181	63	118	119	119	0
MathSATn	0	167	3788.444	3761.619	167	38	129	133	133	0
cvc5	0	133	4510.229	4510.309	133	38	95	167	167	0

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