QF_AX (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +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	Abstained	Timeout	Memout
Yices2-fixedn	0	300	3.741	6.305	300	164	136	0		0	0
Yices2	0	300	3.845	6.256	300	164	136	0		0	0
2019-Yices 2.6.2n	0	300	4.355	6.41	300	164	136	0		0	0
2018-Yicesn	0	300	4.526	6.611	300	164	136	0		0	0
MathSAT5n	0	300	19.961	20.033	300	164	136	0		0	0
z3n	0	300	23.208	23.242	300	164	136	0		0	0
CVC4	0	300	88.543	88.603	300	164	136	0		0	0
SMTInterpol	0	300	467.817	207.531	300	164	136	0		0	0
SMTInterpol-fixedn	0	300	470.203	208.157	300	164	136	0		0	0
Alt-Ergo	0	119	42135.437	27063.242	119	0	119	181		18	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	300	3.845	6.256	300	164	136	0		0	0
Yices2-fixedn	0	300	3.741	6.305	300	164	136	0		0	0
2019-Yices 2.6.2n	0	300	4.355	6.41	300	164	136	0		0	0
2018-Yicesn	0	300	4.526	6.611	300	164	136	0		0	0
MathSAT5n	0	300	19.961	20.033	300	164	136	0		0	0
z3n	0	300	23.208	23.242	300	164	136	0		0	0
CVC4	0	300	88.543	88.603	300	164	136	0		0	0
SMTInterpol	0	300	467.817	207.531	300	164	136	0		0	0
SMTInterpol-fixedn	0	300	470.203	208.157	300	164	136	0		0	0
Alt-Ergo	0	128	52274.557	21535.035	128	0	128	172		9	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	164	0.924	2.663	164	164	0	136	0	0
Yices2-fixedn	0	164	0.883	2.703	164	164	0	136	0	0
2019-Yices 2.6.2n	0	164	1.313	2.738	164	164	0	136	0	0
2018-Yicesn	0	164	1.364	2.775	164	164	0	136	0	0
MathSAT5n	0	164	8.244	8.288	164	164	0	136	0	0
z3n	0	164	8.902	8.923	164	164	0	136	0	0
CVC4	0	164	10.113	10.181	164	164	0	136	0	0
SMTInterpol-fixedn	0	164	131.355	69.412	164	164	0	136	0	0
SMTInterpol	0	164	131.856	69.473	164	164	0	136	0	0
Alt-Ergo	0	0	8158.101	3254.706	0	0	0	300	9	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2	0	136	2.921	3.593	136	0	136	164	0	0
Yices2-fixedn	0	136	2.859	3.602	136	0	136	164	0	0
2019-Yices 2.6.2n	0	136	3.042	3.671	136	0	136	164	0	0
2018-Yicesn	0	136	3.162	3.836	136	0	136	164	0	0
MathSAT5n	0	136	11.717	11.744	136	0	136	164	0	0
z3n	0	136	14.306	14.319	136	0	136	164	0	0
CVC4	0	136	78.429	78.421	136	0	136	164	0	0
SMTInterpol	0	136	335.962	138.057	136	0	136	164	0	0
SMTInterpol-fixedn	0	136	338.848	138.745	136	0	136	164	0	0
Alt-Ergo	0	128	44116.455	18280.329	128	0	128	172	9	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
Yices2	0	300	3.845	6.256	300	164	136	0		0	0
Yices2-fixedn	0	300	3.741	6.305	300	164	136	0		0	0
2019-Yices 2.6.2n	0	300	4.355	6.41	300	164	136	0		0	0
2018-Yicesn	0	300	4.526	6.611	300	164	136	0		0	0
MathSAT5n	0	300	19.961	20.033	300	164	136	0		0	0
z3n	0	300	23.208	23.242	300	164	136	0		0	0
CVC4	0	300	88.543	88.603	300	164	136	0		0	0
SMTInterpol	0	300	467.817	207.531	300	164	136	0		0	0
SMTInterpol-fixedn	0	300	470.203	208.157	300	164	136	0		0	0
Alt-Ergo	0	86	4173.79	2452.375	86	0	86	214		76	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.