QF_ABV (Single Query Track)

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

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

Benchmarks: 2880
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
Bitwuzla	0	2860	37018.143	36994.648	2860	1922	938	20	20	0
2020-Bitwuzlan	0	2859	37954.817	37938.833	2859	1922	937	21	21	0
2020-Yices2-fixedn	0	2850	59372.453	59339.177	2850	1917	933	30	30	0
2020-Yices2n	0	2849	59218.531	59232.236	2849	1917	932	31	31	0
Yices2	0	2847	59801.917	59796.85	2847	1917	930	33	33	0
MathSAT5n	0	2807	111382.887	111464.888	2807	1892	915	73	72	1
z3n	0	2782	139407.319	139458.006	2782	1877	905	98	98	0
cvc5	0	2764	136635.116	159245.245	2764	1863	901	116	116	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla	0	2860	37020.353	36994.088	2860	1922	938	20	20	0
2020-Bitwuzlan	0	2859	37956.507	37937.733	2859	1922	937	21	21	0
2020-Yices2-fixedn	0	2850	59376.643	59337.527	2850	1917	933	30	30	0
2020-Yices2n	0	2849	59223.421	59230.936	2849	1917	932	31	31	0
Yices2	0	2847	59805.017	59795.54	2847	1917	930	33	33	0
MathSAT5n	0	2807	111477.387	111461.528	2807	1892	915	73	72	1
z3n	0	2782	139476.939	139453.456	2782	1877	905	98	98	0
cvc5	0	2764	159125.882	159239.875	2764	1863	901	116	116	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Bitwuzla	0	1922	6200.136	6168.776	1922	1922	0	1	957	20	0
2020-Bitwuzlan	0	1922	7134.526	7115.1	1922	1922	0	1	957	21	0
2020-Yices2n	0	1917	16154.897	16156.039	1917	1917	0	6	957	31	0
2020-Yices2-fixedn	0	1917	16152.483	16159.026	1917	1917	0	6	957	30	0
Yices2	0	1917	16278.284	16289.491	1917	1917	0	6	957	33	0
MathSAT5n	0	1892	49670.032	49672.635	1892	1892	0	31	957	72	1
z3n	0	1877	64332.466	64306.666	1877	1877	0	46	957	98	0
cvc5	0	1863	80659.22	80780.877	1863	1863	0	60	957	116	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
Bitwuzla	0	938	30820.217	30825.312	938	0	938	19	1923	20	0
2020-Bitwuzlan	0	937	30821.981	30822.632	937	0	937	20	1923	21	0
2020-Yices2-fixedn	0	933	43224.16	43178.501	933	0	933	24	1923	30	0
2020-Yices2n	0	932	43068.523	43074.896	932	0	932	25	1923	31	0
Yices2	0	930	43526.734	43506.049	930	0	930	27	1923	33	0
MathSAT5n	0	915	61807.355	61788.894	915	0	915	42	1923	72	1
z3n	0	905	75144.473	75146.789	905	0	905	52	1923	98	0
cvc5	0	901	78466.662	78458.998	901	0	901	56	1923	116	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Bitwuzla	0	2797	3377.304	3348.502	2797	1886	911	83	83	0
2020-Bitwuzlan	0	2790	3409.303	3412.263	2790	1880	910	90	90	0
2020-Yices2-fixedn	0	2767	3894.824	3903.508	2767	1881	886	113	113	0
2020-Yices2n	0	2767	3901.512	3904.793	2767	1881	886	113	113	0
Yices2	0	2767	3905.686	3920.287	2767	1881	886	113	113	0
MathSAT5n	0	2707	6406.834	6386.015	2707	1836	871	173	172	1
z3n	0	2705	5715.641	5688.38	2705	1838	867	175	175	0
cvc5	0	2682	9014.262	8930.825	2682	1818	864	198	198	0

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