QF_ABVFP (Single Query Track)

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

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

Benchmarks: 619
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Bitwuzla-fixedn	0	617	5299.597	5300.768	617	121	496	2	2	0
2020-Bitwuzlan	0	617	5364.612	5321.948	617	121	496	2	2	0
Bitwuzla	0	617	6386.64	6386.939	617	121	496	2	2	0
MathSAT5n	0	612	14294.309	14233.626	612	121	491	7	7	0
2020-MathSAT5n	0	612	14474.319	14339.69	612	121	491	7	7	0
2020-CVC4n	0	608	18917.683	18873.973	608	119	489	11	11	0
cvc5	0	608	24853.809	24798.494	608	119	489	11	11	0
COLIBRI - fixedn	0	511	24284.992	24284.107	511	109	402	108	15	0
2020-COLIBRIn	0	504	32419.444	32377.118	504	109	395	115	25	0
COLIBRI	3	507	24927.151	24878.896	507	105	402	112	16	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Bitwuzla-fixedn	0	617	5300.037	5300.738	617	121	496	2	2	0
2020-Bitwuzlan	0	617	5364.992	5321.878	617	121	496	2	2	0
Bitwuzla	0	617	6387.31	6386.859	617	121	496	2	2	0
MathSAT5n	0	612	14295.779	14233.396	612	121	491	7	7	0
2020-MathSAT5n	0	612	14475.999	14339.24	612	121	491	7	7	0
2020-CVC4n	0	608	18920.843	18873.513	608	119	489	11	11	0
cvc5	0	608	24855.229	24798.014	608	119	489	11	11	0
COLIBRI - fixedn	0	511	24286.172	24283.417	511	109	402	108	15	0
2020-COLIBRIn	0	504	32422.044	32376.638	504	109	395	115	25	0
COLIBRI	3	507	24929.291	24878.566	507	105	402	112	16	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-Bitwuzla-fixedn	0	121	192.725	193.051	121	121	0	0	498	2	0
2020-Bitwuzlan	0	121	193.767	193.888	121	121	0	0	498	2	0
Bitwuzla	0	121	200.063	200.162	121	121	0	0	498	2	0
MathSAT5n	0	121	639.399	639.567	121	121	0	0	498	7	0
2020-MathSAT5n	0	121	669.155	667.223	121	121	0	0	498	7	0
2020-CVC4n	0	119	3167.154	3167.39	119	119	0	2	498	11	0
cvc5	0	119	3368.371	3365.301	119	119	0	2	498	11	0
2020-COLIBRIn	0	109	3917.729	3891.405	109	109	0	12	498	25	0
COLIBRI - fixedn	0	109	5304.502	5307.979	109	109	0	12	498	15	0
COLIBRI	0	105	6550.765	6515.127	105	105	0	16	498	16	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-Bitwuzla-fixedn	0	496	2707.313	2707.686	496	0	496	0	123	2	0
2020-Bitwuzlan	0	496	2771.225	2727.99	496	0	496	0	123	2	0
Bitwuzla	0	496	3787.247	3786.697	496	0	496	0	123	2	0
MathSAT5n	0	491	11256.381	11193.829	491	0	491	5	123	7	0
2020-MathSAT5n	0	491	11406.844	11272.017	491	0	491	5	123	7	0
2020-CVC4n	0	489	13353.689	13306.123	489	0	489	7	123	11	0
cvc5	0	489	19086.858	19032.712	489	0	489	7	123	11	0
COLIBRI - fixedn	0	402	16581.67	16575.438	402	0	402	94	123	15	0
2020-COLIBRIn	0	395	26391.355	26372.135	395	0	395	101	123	25	0
COLIBRI	3	402	15978.526	15963.438	402	0	402	94	123	16	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Bitwuzla-fixedn	0	603	1031.076	1031.493	603	120	483	16	16	0
2020-Bitwuzlan	0	602	1039.195	1030.367	602	119	483	17	17	0
Bitwuzla	0	601	1073.038	1072.227	601	119	482	18	18	0
MathSAT5n	0	588	2510.402	2496.563	588	117	471	31	31	0
2020-MathSAT5n	0	586	2611.687	2559.391	586	117	469	33	33	0
2020-CVC4n	0	574	2790.597	2774.072	574	113	461	45	45	0
cvc5	0	503	4720.773	4702.128	503	111	392	116	116	0
COLIBRI - fixedn	0	501	2008.547	2004.727	501	102	399	118	29	0
2020-COLIBRIn	0	495	1846.198	1827.143	495	106	389	124	35	0
COLIBRI	3	499	1969.177	1951.079	499	99	400	120	28	0

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