QF_UFBV (Single Query Track)

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

Page generated on 2021-07-18 17:29:07 +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)
Bitwuzla	Bitwuzla	Bitwuzla	Bitwuzla	Yices2

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Bitwuzlan	0	288	17603.503	17578.776	288	163	125	12	5	0
Bitwuzla	0	286	44136.186	44085.63	286	162	124	14	14	0
cvc5	0	261	78005.906	78007.914	261	152	109	39	39	0
2020-Yices2n	0	251	85127.472	85136.655	251	162	89	49	49	0
2020-Yices2-fixedn	0	250	85535.754	85533.792	250	162	88	50	50	0
Yices2	0	249	85015.687	84993.698	249	162	87	51	51	0
z3n	0	246	84393.371	84403.825	246	142	104	54	54	0
MathSAT5n	0	237	96298.654	96287.23	237	145	92	63	63	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Bitwuzlan	0	288	17604.123	17578.616	288	163	125	12	5	0
Bitwuzla	0	286	44137.446	44085.04	286	162	124	14	14	0
cvc5	0	261	78014.326	78006.424	261	152	109	39	39	0
2020-Yices2n	0	251	85132.022	85134.955	251	162	89	49	49	0
2020-Yices2-fixedn	0	250	85540.664	85532.172	250	162	88	50	50	0
Yices2	0	249	85019.377	84992.338	249	162	87	51	51	0
z3n	0	246	84401.371	84401.725	246	142	104	54	54	0
MathSAT5n	0	237	96312.534	96284.36	237	145	92	63	63	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-Bitwuzlan	0	163	3194.878	3195.226	163	163	0	1	136	5	0
Bitwuzla	0	162	4058.879	4025.177	162	162	0	2	136	14	0
2020-Yices2n	0	162	4512.055	4512.479	162	162	0	2	136	49	0
Yices2	0	162	4527.322	4527.686	162	162	0	2	136	51	0
2020-Yices2-fixedn	0	162	4538.997	4528.478	162	162	0	2	136	50	0
cvc5	0	152	21182.657	21180.103	152	152	0	12	136	39	0
MathSAT5n	0	145	24138.341	24124.757	145	145	0	19	136	63	0
z3n	0	142	30668.564	30666.523	142	142	0	22	136	54	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-Bitwuzlan	0	125	14409.245	14383.39	125	0	125	11	164	5	0
Bitwuzla	0	124	40078.567	40059.863	124	0	124	12	164	14	0
cvc5	0	109	56831.669	56826.321	109	0	109	27	164	39	0
z3n	0	104	53732.808	53735.202	104	0	104	32	164	54	0
MathSAT5n	0	92	72174.193	72159.603	92	0	92	44	164	63	0
2020-Yices2n	0	89	80619.967	80622.476	89	0	89	47	164	49	0
2020-Yices2-fixedn	0	88	81001.667	81003.694	88	0	88	48	164	50	0
Yices2	0	87	80492.055	80464.653	87	0	87	49	164	51	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
2020-Yices2n	0	195	2857.556	2857.729	195	151	44	105	105	0
2020-Yices2-fixedn	0	195	2868.521	2857.757	195	151	44	105	105	0
Yices2	0	195	2862.734	2862.775	195	151	44	105	105	0
2020-Bitwuzlan	0	195	3021.718	3021.871	195	136	59	105	98	0
Bitwuzla	0	189	3250.698	3227.794	189	136	53	111	111	0
MathSAT5n	0	169	3747.477	3715.387	169	129	40	131	131	0
z3n	0	147	4356.688	4354.004	147	111	36	153	153	0
cvc5	0	142	4640.499	4625.851	142	107	35	158	158	0

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