QF_AX (Single Query Track)

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

Page generated on 2021-07-18 17:29:06 +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
2020-Yices2-fixedn	0	300	4.161	5.601	300	169	131	0	0	0
2020-Yices2n	0	300	4.169	5.646	300	169	131	0	0	0
Yices2	0	300	4.316	6.994	300	169	131	0	0	0
MathSAT5n	0	300	20.716	20.771	300	169	131	0	0	0
z3n	0	300	21.841	21.887	300	169	131	0	0	0
2020-z3n	0	300	29.383	29.405	300	169	131	0	0	0
cvc5	0	300	125.607	125.57	300	169	131	0	0	0
SMTInterpol	0	300	530.635	219.618	300	169	131	0	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Yices2-fixedn	0	300	4.161	5.601	300	169	131	0	0	0
2020-Yices2n	0	300	4.169	5.646	300	169	131	0	0	0
Yices2	0	300	4.316	6.994	300	169	131	0	0	0
MathSAT5n	0	300	20.716	20.771	300	169	131	0	0	0
z3n	0	300	21.841	21.887	300	169	131	0	0	0
2020-z3n	0	300	29.383	29.405	300	169	131	0	0	0
cvc5	0	300	125.607	125.57	300	169	131	0	0	0
SMTInterpol	0	300	530.635	219.618	300	169	131	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
2020-Yices2-fixedn	0	169	0.944	2.074	169	169	0	0	131	0	0
2020-Yices2n	0	169	0.98	2.136	169	169	0	0	131	0	0
Yices2	0	169	0.978	2.962	169	169	0	0	131	0	0
z3n	0	169	6.458	6.472	169	169	0	0	131	0	0
MathSAT5n	0	169	8.071	8.081	169	169	0	0	131	0	0
2020-z3n	0	169	9.023	9.034	169	169	0	0	131	0	0
cvc5	0	169	10.922	10.854	169	169	0	0	131	0	0
SMTInterpol	0	169	142.989	73.845	169	169	0	0	131	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
2020-Yices2n	0	131	3.189	3.511	131	0	131	0	169	0	0
2020-Yices2-fixedn	0	131	3.217	3.527	131	0	131	0	169	0	0
Yices2	0	131	3.338	4.032	131	0	131	0	169	0	0
MathSAT5n	0	131	12.645	12.69	131	0	131	0	169	0	0
z3n	0	131	15.384	15.414	131	0	131	0	169	0	0
2020-z3n	0	131	20.36	20.371	131	0	131	0	169	0	0
cvc5	0	131	114.685	114.716	131	0	131	0	169	0	0
SMTInterpol	0	131	387.646	145.773	131	0	131	0	169	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Yices2-fixedn	0	300	4.161	5.601	300	169	131	0	0	0
2020-Yices2n	0	300	4.169	5.646	300	169	131	0	0	0
Yices2	0	300	4.316	6.994	300	169	131	0	0	0
MathSAT5n	0	300	20.716	20.771	300	169	131	0	0	0
z3n	0	300	21.841	21.887	300	169	131	0	0	0
2020-z3n	0	300	29.383	29.405	300	169	131	0	0	0
SMTInterpol	0	300	530.635	219.618	300	169	131	0	0	0
cvc5	0	298	119.965	119.921	298	169	129	2	2	0

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