QF_ALIA (Single Query Track)

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

Page generated on 2021-07-18 17:29:05 +0000

Benchmarks: 116
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
2019-Yices 2.6.2n	0	116	54.288	54.523	116	54	62	0	0	0
Yices2	0	116	65.94	66.409	116	54	62	0	0	0
MathSAT5n	0	116	111.576	105.051	116	54	62	0	0	0
z3n	0	116	923.683	888.704	116	54	62	0	0	0
SMTInterpol	0	116	1049.122	522.623	116	54	62	0	0	0
cvc5 - fixedn	0	115	6063.8	6064.632	115	54	61	1	1	0
cvc5	0	111	4680.756	9981.873	111	50	61	5	5	0
veriT	0	6	4.7	4.873	6	0	6	110	0	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Yices 2.6.2n	0	116	54.288	54.523	116	54	62	0	0	0
Yices2	0	116	65.94	66.409	116	54	62	0	0	0
MathSAT5n	0	116	111.576	105.051	116	54	62	0	0	0
SMTInterpol	0	116	1049.122	522.623	116	54	62	0	0	0
z3n	0	116	923.683	888.704	116	54	62	0	0	0
cvc5 - fixedn	0	115	6063.88	6064.612	115	54	61	1	1	0
cvc5	0	111	9980.718	9981.603	111	50	61	5	5	0
veriT	0	6	4.7	4.873	6	0	6	110	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
2019-Yices 2.6.2n	0	54	48.039	48.048	54	54	0	0	62	0	0
Yices2	0	54	59.359	59.392	54	54	0	0	62	0	0
MathSAT5n	0	54	76.005	69.462	54	54	0	0	62	0	0
SMTInterpol	0	54	478.868	164.818	54	54	0	0	62	0	0
z3n	0	54	856.89	824.514	54	54	0	0	62	0	0
cvc5 - fixedn	0	54	3246.606	3247.194	54	54	0	0	62	1	0
cvc5	0	50	7182.381	7182.932	50	50	0	4	62	5	0
veriT	0	0	2.526	2.533	0	0	0	54	62	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
2019-Yices 2.6.2n	0	62	6.249	6.475	62	0	62	0	54	0	0
Yices2	0	62	6.581	7.017	62	0	62	0	54	0	0
MathSAT5n	0	62	35.572	35.589	62	0	62	0	54	0	0
z3n	0	62	66.793	64.19	62	0	62	0	54	0	0
SMTInterpol	0	62	570.254	357.805	62	0	62	0	54	0	0
cvc5	0	61	2798.337	2798.671	61	0	61	1	54	5	0
cvc5 - fixedn	0	61	2817.274	2817.418	61	0	61	1	54	1	0
veriT	0	6	2.174	2.34	6	0	6	56	54	0	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2019-Yices 2.6.2n	0	116	54.288	54.523	116	54	62	0	0	0
Yices2	0	116	65.94	66.409	116	54	62	0	0	0
MathSAT5n	0	116	111.576	105.051	116	54	62	0	0	0
SMTInterpol	0	113	812.745	352.238	113	54	59	3	3	0
z3n	0	104	511.428	505.054	104	43	61	12	12	0
cvc5	0	89	684.99	684.96	89	36	53	27	27	0
cvc5 - fixedn	0	89	685.233	685.193	89	36	53	27	27	0
veriT	0	6	4.7	4.873	6	0	6	110	0	0

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