QF_UFNIA (Single Query Track)

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

Page generated on 2021-07-18 17:29:07 +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	Yices2	cvc5	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	296	4817.674	4818.339	296	221	75	4	4	0
2020-CVC4n	0	287	1317.419	1296.489	287	216	71	13	1	0
2019-CVC4n	0	284	6093.315	6094.402	284	215	69	16	5	0
Yices2	0	282	21724.225	21728.623	282	220	62	18	18	0
cvc5	0	270	3697.301	3698.156	270	204	66	30	3	0
cvc5 - fixedn	0	270	3698.655	3698.399	270	204	66	30	3	0
MathSAT5n	0	243	33335.659	33341.419	243	186	57	57	27	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	296	4818.234	4818.259	296	221	75	4	4	0
2020-CVC4n	0	287	1317.529	1296.459	287	216	71	13	1	0
2019-CVC4n	0	284	6094.295	6094.222	284	215	69	16	5	0
Yices2	0	282	21727.365	21727.913	282	220	62	18	18	0
cvc5	0	270	3698.041	3697.916	270	204	66	30	3	0
cvc5 - fixedn	0	270	3699.175	3698.059	270	204	66	30	3	0
MathSAT5n	0	243	33340.189	33340.379	243	186	57	57	27	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3n	0	221	14.627	14.644	221	221	0	0	79	4	0
Yices2	0	220	1325.413	1325.77	220	220	0	1	79	18	0
2020-CVC4n	0	216	63.518	42.466	216	216	0	5	79	1	0
2019-CVC4n	0	215	4876.58	4876.527	215	215	0	6	79	5	0
cvc5	0	204	2467.687	2467.591	204	204	0	17	79	3	0
cvc5 - fixedn	0	204	2468.715	2467.63	204	204	0	17	79	3	0
MathSAT5n	0	186	18816.45	18816.591	186	186	0	35	79	27	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3n	0	75	1203.607	1203.615	75	0	75	1	224	4	0
2020-CVC4n	0	71	1206.142	1206.116	71	0	71	5	224	1	0
2019-CVC4n	0	69	1206.335	1206.316	69	0	69	7	224	5	0
cvc5	0	66	1229.794	1229.767	66	0	66	10	224	3	0
cvc5 - fixedn	0	66	1229.843	1229.809	66	0	66	10	224	3	0
Yices2	0	62	16801.952	16802.143	62	0	62	14	224	18	0
MathSAT5n	0	57	10923.738	10923.789	57	0	57	19	224	27	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	296	114.234	114.259	296	221	75	4	4	0
2020-CVC4n	0	287	132.249	111.178	287	216	71	13	2	0
2019-CVC4n	0	283	179.721	179.645	283	214	69	17	6	0
Yices2	0	280	501.817	502.363	280	218	62	20	20	0
cvc5	0	269	168.764	168.637	269	204	65	31	4	0
cvc5 - fixedn	0	269	169.839	168.719	269	204	65	31	4	0
MathSAT5n	0	240	906.646	906.76	240	185	55	60	30	0

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