Largest Contribution Ranking - Single Query Track

Page generated on 2023-07-06 16:05:13 +0000

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
cvc5	cvc5	cvc5	cvc5	cvc5

Sequential Performance

Solver	Correct Score	Time Score	Division
cvc5	0.03146325	0.01251903	Equality
cvc5	0.02855388	0.0060313	Equality+MachineArith
cvc5	0.01566994	0.0274028	Equality+NonLinearArith
cvc5	0.01416832	0.04112914	Equality+LinearArith
Z3++	0.00262965	0.02055604	QF_NonLinearIntArith
Bitwuzla	0.00200413	0.00948228	FPArith
YicesQS	0.00186045	0.02226213	Arith
Bitwuzla	0.00118404	0.0120762	QF_FPArith
Z3++	0.00086703	0.01597785	QF_LinearIntArith
cvc5	0.00077048	0.00676229	Bitvec
cvc5	0.00065615	-0.01319877	QF_Equality+Bitvec
SMTInterpol	0.00030175	0.00464193	QF_Equality+LinearArith
Z3++	0.0002899	0.0042593	QF_NonLinearRealArith
cvc5	0.00027515	0.00124247	QF_Equality+NonLinearArith
STP	0.00024832	0.01410421	QF_Bitvec
OpenSMT	9.377e-05	0.0020649	QF_LinearRealArith
Yices2	0.0	0.03309434	QF_Equality

Parallel Performance

Solver	Correct Score	Time Score	Division
cvc5	0.04693491	0.01703638	Equality
cvc5	0.03051732	0.06214593	Equality+LinearArith
cvc5	0.02855388	0.00596909	Equality+MachineArith
cvc5	0.01210123	0.02247147	Equality+NonLinearArith
Z3++	0.00262965	0.02056228	QF_NonLinearIntArith
Bitwuzla	0.00200413	0.00949128	FPArith
YicesQS	0.00186045	0.02224015	Arith
Bitwuzla	0.00118404	0.01207794	QF_FPArith
Z3++	0.00086703	0.01595678	QF_LinearIntArith
cvc5	0.00077048	0.00674825	Bitvec
cvc5	0.00065615	-0.01322457	QF_Equality+Bitvec
SMTInterpol	0.00031199	0.00509063	QF_Equality+LinearArith
Z3++	0.0002899	0.00426403	QF_NonLinearRealArith
cvc5	0.00027515	0.0012496	QF_Equality+NonLinearArith
STP	0.00024832	0.0138953	QF_Bitvec
OpenSMT	9.377e-05	0.00205499	QF_LinearRealArith
Yices2	0.0	0.0329754	QF_Equality

SAT Performance

Solver	Correct Score	Time Score	Division
cvc5	0.041491	0.00329091	Equality+NonLinearArith
cvc5	0.04007647	0.00192523	Equality+LinearArith
cvc5	0.03147117	-0.00287519	Equality+MachineArith
cvc5	0.01259513	0.00127793	Equality
Bitwuzla	0.00426264	0.0017574	FPArith
Z3++	0.00294951	0.00738741	QF_NonLinearIntArith
YicesQS	0.00220737	0.00139234	Arith
Z3++	0.00103917	0.00158565	QF_LinearIntArith
cvc5	0.00092473	-0.00129502	QF_Equality+Bitvec
Bitwuzla	0.00077161	0.0004449	QF_FPArith
Bitwuzla	0.00053955	0.00029818	Bitvec
Z3++	0.00051054	0.00048597	QF_NonLinearRealArith
SMTInterpol	0.00043819	0.00049004	QF_Equality+LinearArith
Bitwuzla	0.00019215	0.00026523	QF_Bitvec
Yices2	0.0001431	0.0002837	QF_Equality+NonLinearArith
OpenSMT	9.577e-05	0.00015644	QF_LinearRealArith
Yices2	0.0	3.11e-06	QF_Equality

UNSAT Performance

Solver	Correct Score	Time Score	Division
cvc5	0.04001813	0.01209227	Equality
cvc5	0.0287424	0.05007326	Equality+LinearArith
cvc5	0.02323101	0.00625521	Equality+MachineArith
cvc5	0.00830851	0.01371948	Equality+NonLinearArith
Z3++	0.00193396	0.00072605	QF_NonLinearIntArith
YicesQS	0.00165128	0.00274006	Arith
Bitwuzla	0.00142509	0.00204122	QF_FPArith
Bitwuzla	0.00090846	0.00152764	FPArith
cvc5	0.00083223	0.00025217	QF_Equality+NonLinearArith
Z3++	0.00057129	0.00036899	QF_LinearIntArith
Bitwuzla	0.00038434	0.00051414	QF_Equality+Bitvec
STP	0.00036137	0.00059017	QF_Bitvec
cvc5	0.0003027	0.00063646	Bitvec
cvc5-NRA-LS	0.00026015	0.00038863	QF_NonLinearRealArith
OpenSMT	0.00021747	0.00013351	QF_Equality+LinearArith
OpenSMT	9.124e-05	0.00018966	QF_LinearRealArith
Yices2	0.0	7.767e-05	QF_Equality

24s Performance

Solver	Correct Score	Time Score	Division
cvc5	0.0280728	0.03157577	Equality+NonLinearArith
cvc5	0.0273453	0.00144767	Equality+MachineArith
cvc5	0.01867736	0.0421294	Equality+LinearArith
Vampire	0.01638628	0.00779617	Equality
Z3++	0.01200778	0.03132467	QF_NonLinearIntArith
Yices2	0.00961171	0.04652817	QF_LinearIntArith
YicesQS	0.00304568	0.02230633	Arith
Bitwuzla	0.00252949	0.00774426	FPArith
STP	0.00144345	0.01948662	QF_Bitvec
Bitwuzla	0.00131927	0.00976633	QF_FPArith
Bitwuzla	0.00119926	0.00643363	Bitvec
Bitwuzla	0.00076897	0.00426132	QF_Equality+Bitvec
Yices2	0.00067047	0.00228277	QF_LinearRealArith
Z3++	0.00063153	0.00459796	QF_NonLinearRealArith
Yices2	0.00034444	0.00310738	QF_Equality+LinearArith
Yices2	0.00031468	0.03564485	QF_Equality
cvc5	0.00027468	0.00085458	QF_Equality+NonLinearArith

n Non-competing.
e Experimental.