QF_UFLIA (Single Query Track)

Competition results for the QF_UFLIA 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	Yices2	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	300	61.324	61.361	300	238	62	0	0	0
2018-Yicesn	0	300	67.685	64.858	300	238	62	0	0	0
Yices2	0	300	79.66	79.573	300	238	62	0	0	0
cvc5 - fixedn	0	300	544.249	544.271	300	238	62	0	0	0
cvc5	0	300	548.988	548.984	300	238	62	0	0	0
SMTInterpol	0	300	1775.701	980.197	300	238	62	0	0	0
MathSAT5n	0	299	3676.243	3676.928	299	238	61	1	1	0
veriT	0	257	37591.963	37594.658	257	197	60	43	13	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3n	0	300	61.324	61.361	300	238	62	0	0	0
2018-Yicesn	0	300	67.685	64.858	300	238	62	0	0	0
Yices2	0	300	79.66	79.573	300	238	62	0	0	0
cvc5 - fixedn	0	300	544.249	544.271	300	238	62	0	0	0
cvc5	0	300	548.988	548.984	300	238	62	0	0	0
SMTInterpol	0	300	1775.701	980.197	300	238	62	0	0	0
MathSAT5n	0	299	3676.303	3676.908	299	238	61	1	1	0
veriT	0	257	37592.533	37594.328	257	197	60	43	13	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
2018-Yicesn	0	238	5.873	6.184	238	238	0	0	62	0	0
Yices2	0	238	5.608	6.334	238	238	0	0	62	0	0
z3n	0	238	27.603	27.635	238	238	0	0	62	0	0
cvc5	0	238	190.453	190.42	238	238	0	0	62	0	0
cvc5 - fixedn	0	238	191.947	191.884	238	238	0	0	62	0	0
SMTInterpol	0	238	1058.036	515.13	238	238	0	0	62	0	0
MathSAT5n	0	238	1868.161	1868.693	238	238	0	0	62	1	0
veriT	0	197	31327.578	31329.143	197	197	0	41	62	13	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	62	33.721	33.726	62	0	62	0	238	0	0
2018-Yicesn	0	62	61.813	58.673	62	0	62	0	238	0	0
Yices2	0	62	74.052	73.239	62	0	62	0	238	0	0
cvc5 - fixedn	0	62	352.301	352.386	62	0	62	0	238	0	0
cvc5	0	62	358.535	358.565	62	0	62	0	238	0	0
SMTInterpol	0	62	717.664	465.068	62	0	62	0	238	0	0
MathSAT5n	0	61	1808.141	1808.215	61	0	61	1	238	1	0
veriT	0	60	6264.955	6265.185	60	0	60	2	238	13	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	300	61.324	61.361	300	238	62	0	0	0
2018-Yicesn	0	299	54.979	52.148	299	238	61	1	1	0
Yices2	0	299	59.623	59.533	299	238	61	1	1	0
cvc5	0	295	413.639	413.609	295	238	57	5	5	0
cvc5 - fixedn	0	295	415.797	415.778	295	238	57	5	5	0
SMTInterpol	0	290	1217.103	617.641	290	234	56	10	10	0
MathSAT5n	0	284	523.884	524.269	284	226	58	16	16	0
veriT	0	180	3526.936	3526.996	180	130	50	120	109	0

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