QF_UFNIA (Single Query Track)

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

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

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

Winners

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

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	243	7250.741	7250.12	243	173	70	6	6	0
cvc5	0	231	21956.414	21960.542	231	166	65	18	18	0
2020-CVC4n	0	226	3662.952	3663.129	226	162	64	23	3	0
Yices2	0	222	32628.843	32633.914	222	172	50	27	27	0
MathSATn	0	162	50060.564	50066.397	162	115	47	87	41	0
smtinterpol	0	71	160.968	101.129	71	55	16	178	0	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	243	7251.441	7249.96	243	173	70	6	6	0
cvc5	0	231	21959.654	21959.692	231	166	65	18	18	0
2020-CVC4n	0	226	3663.112	3663.079	226	162	64	23	3	0
Yices2	0	222	32632.753	32632.924	222	172	50	27	27	0
MathSATn	0	162	50064.494	50064.687	162	115	47	87	41	0
smtinterpol	0	71	160.968	101.129	71	55	16	178	0	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-4.8.17n	0	173	45.317	45.025	173	173	0	0	76	6	0
Yices2	0	172	1430.912	1431.01	172	172	0	1	76	27	0
cvc5	0	166	8615.871	8615.893	166	166	0	7	76	18	0
2020-CVC4n	0	162	2454.584	2454.563	162	162	0	11	76	3	0
MathSATn	0	115	33236.141	33236.321	115	115	0	58	76	41	0
smtinterpol	0	55	110.929	70.021	55	55	0	118	76	0	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-4.8.17n	0	70	1206.124	1204.935	70	0	70	1	178	6	0
cvc5	0	65	7343.783	7343.799	65	0	65	6	178	18	0
2020-CVC4n	0	64	7.401	7.388	64	0	64	7	178	3	0
Yices2	0	50	25201.842	25201.913	50	0	50	21	178	27	0
MathSATn	0	47	10828.353	10828.366	47	0	47	24	178	41	0
smtinterpol	0	16	47.174	29.214	16	0	16	55	178	0	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	242	188.709	187.226	242	172	70	7	7	0
cvc5	0	228	660.239	660.225	228	164	64	21	21	0
2020-CVC4n	0	225	124.539	124.503	225	161	64	24	4	0
Yices2	0	218	754.451	754.6	218	168	50	31	31	0
MathSATn	0	157	1275.365	1275.47	157	110	47	92	46	0
smtinterpol	0	71	160.968	101.129	71	55	16	178	0	0

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