QF_AX (Single Query Track)

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

Page generated on 2022-08-10 11:17:44 +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
Yices2	0	300	5.515	6.748	300	131	169	0	0	0
z3-4.8.17n	0	300	25.444	24.946	300	131	169	0	0	0
MathSATn	0	300	26.669	26.743	300	131	169	0	0	0
2021-z3n	0	300	27.104	23.884	300	131	169	0	0	0
cvc5	0	300	202.748	202.71	300	131	169	0	0	0
OpenSMT	0	300	287.501	286.79	300	131	169	0	0	0
OpenSMT-fixedn	0	300	454.197	439.238	300	131	169	0	0	0
smtinterpol	0	300	945.73	375.384	300	131	169	0	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	300	5.515	6.748	300	131	169	0	0	0
2021-z3n	0	300	27.104	23.884	300	131	169	0	0	0
z3-4.8.17n	0	300	25.444	24.946	300	131	169	0	0	0
MathSATn	0	300	26.669	26.743	300	131	169	0	0	0
cvc5	0	300	202.748	202.71	300	131	169	0	0	0
OpenSMT	0	300	287.501	286.79	300	131	169	0	0	0
smtinterpol	0	300	945.73	375.384	300	131	169	0	0	0
OpenSMT-fixedn	0	300	454.197	439.238	300	131	169	0	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
Yices2	0	131	0.88	1.758	131	131	0	0	169	0	0
2021-z3n	0	131	5.367	5.376	131	131	0	0	169	0	0
z3-4.8.17n	0	131	6.097	5.872	131	131	0	0	169	0	0
MathSATn	0	131	8.211	8.238	131	131	0	0	169	0	0
cvc5	0	131	17.625	17.58	131	131	0	0	169	0	0
OpenSMT	0	131	24.284	23.446	131	131	0	0	169	0	0
OpenSMT-fixedn	0	131	23.731	23.918	131	131	0	0	169	0	0
smtinterpol	0	131	160.82	76.056	131	131	0	0	169	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
Yices2	0	169	4.635	4.989	169	0	169	0	131	0	0
MathSATn	0	169	18.459	18.505	169	0	169	0	131	0	0
2021-z3n	0	169	21.736	18.507	169	0	169	0	131	0	0
z3-4.8.17n	0	169	19.347	19.075	169	0	169	0	131	0	0
cvc5	0	169	185.122	185.129	169	0	169	0	131	0	0
OpenSMT	0	169	263.217	263.344	169	0	169	0	131	0	0
smtinterpol	0	169	784.91	299.328	169	0	169	0	131	0	0
OpenSMT-fixedn	0	169	430.467	415.321	169	0	169	0	131	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	300	5.515	6.748	300	131	169	0	0	0
2021-z3n	0	300	27.104	23.884	300	131	169	0	0	0
z3-4.8.17n	0	300	25.444	24.946	300	131	169	0	0	0
MathSATn	0	300	26.669	26.743	300	131	169	0	0	0
smtinterpol	0	300	945.73	375.384	300	131	169	0	0	0
OpenSMT	0	299	281.608	280.89	299	131	168	1	1	0
cvc5	0	298	187.288	187.229	298	131	167	2	2	0
OpenSMT-fixedn	0	297	395.676	380.702	297	131	166	3	3	0

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