QF_RDL (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

Benchmarks: 247
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
2019-Yices 2.6.2n	0	213	42884.954	42888.317	213	105	108	34		34	0
Yices2	0	213	43119.556	43110.459	213	105	108	34		34	0
Yices2-fixedn	0	213	43120.051	43122.615	213	105	108	34		34	0
CVC4	0	209	52520.291	52520.204	209	102	107	38		38	0
z3n	0	207	53535.916	53456.854	207	99	108	40		40	0
veriT	0	206	55093.107	55099.727	206	102	104	41		41	0
MathSAT5n	0	198	66820.566	66785.806	198	102	96	49		49	0
SMTInterpol	0	187	88612.642	87026.635	187	97	90	60		60	0
SMTInterpol-fixedn	0	187	88722.538	87146.632	187	97	90	60		60	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Yices 2.6.2n	0	213	42887.264	42887.547	213	105	108	34		34	0
Yices2	0	213	43121.186	43109.919	213	105	108	34		34	0
Yices2-fixedn	0	213	43122.521	43121.895	213	105	108	34		34	0
CVC4	0	209	52523.661	52518.824	209	102	107	38		38	0
z3n	0	207	53541.516	53455.484	207	99	108	40		40	0
veriT	0	206	55097.727	55098.427	206	102	104	41		41	0
MathSAT5n	0	198	66828.686	66784.066	198	102	96	49		49	0
SMTInterpol	0	187	88612.642	87026.635	187	97	90	60		60	0
SMTInterpol-fixedn	0	187	88722.538	87146.632	187	97	90	60		60	0

SAT 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	105	466.779	466.885	105	105	0	142	34	0
Yices2-fixedn	0	105	494.354	494.497	105	105	0	142	34	0
Yices2	0	105	495.218	495.303	105	105	0	142	34	0
veriT	0	102	6701.181	6701.613	102	102	0	145	41	0
CVC4	0	102	6982.237	6976.905	102	102	0	145	38	0
MathSAT5n	0	102	7719.635	7720.442	102	102	0	145	49	0
z3n	0	99	9439.553	9354.514	99	99	0	148	40	0
SMTInterpol	0	97	15648.538	14844.273	97	97	0	150	60	0
SMTInterpol-fixedn	0	97	15665.129	14866.764	97	97	0	150	60	0

UNSAT 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	108	2820.485	2820.662	108	0	108	139	34	0
Yices2	0	108	3025.968	3014.615	108	0	108	139	34	0
Yices2-fixedn	0	108	3028.167	3027.398	108	0	108	139	34	0
z3n	0	108	4501.963	4500.97	108	0	108	139	40	0
CVC4	0	107	5941.424	5941.919	107	0	107	140	38	0
veriT	0	104	8796.546	8796.814	104	0	104	143	41	0
MathSAT5n	0	96	19509.052	19463.624	96	0	96	151	49	0
SMTInterpol	0	90	33364.104	32582.362	90	0	90	157	60	0
SMTInterpol-fixedn	0	90	33457.409	32679.867	90	0	90	157	60	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Yices 2.6.2n	0	193	1631.563	1631.729	193	98	95	54		54	0
Yices2	0	191	1675.275	1663.873	191	98	93	56		56	0
Yices2-fixedn	0	191	1665.46	1664.658	191	98	93	56		56	0
z3n	0	180	2164.244	2136.677	180	88	92	67		67	0
veriT	0	169	2304.838	2304.861	169	82	87	78		78	0
MathSAT5n	0	165	2471.205	2467.35	165	89	76	82		82	0
CVC4	0	165	2563.289	2557.185	165	85	80	82		82	0
SMTInterpol	0	132	4090.097	3365.351	132	72	60	115		115	0
SMTInterpol-fixedn	0	132	4066.534	3368.687	132	72	60	115		115	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.