QF_SLIA (Single Query Track)

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

Page generated on 2023-07-06 16:04:54 +0000

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
cvc5	cvc5	cvc5	cvc5	z3-alpha

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	21446	493777.744	501432.743	21446	14069	7377	492	489	0
2022-cvc5n	0	20961	536412.42	544016.2	20961	13853	7108	977	975	0
z3-alpha	0	20897	179385.088	178930.361	20897	13599	7298	1041	802	0
OSTRICH Fixedn	0	16916	480139.722	256427.896	16916	9560	7356	5022	5016	0
Z3-Noodler Fixedn	1	12711	205466.561	205392.597	12711	7344	5367	9227	2042	4276
Z3-Noodler	5	12771	194846.172	194853.779	12771	7406	5365	9167	1987	4334
OSTRICH	10	16802	431958.418	224983.311	16802	9445	7357	5136	5045	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	21446	493777.744	501432.743	21446	14069	7377	492	489	0
2022-cvc5n	0	20961	536412.42	544016.2	20961	13853	7108	977	975	0
z3-alpha	0	20897	179385.088	178930.361	20897	13599	7298	1041	802	0
OSTRICH Fixedn	0	16942	519856.632	280959.4	16942	9586	7356	4996	4990	0
Z3-Noodler Fixedn	1	12711	205466.561	205392.597	12711	7344	5367	9227	2042	4276
Z3-Noodler	5	12770	193646.192	193653.759	12770	7405	5365	9168	1988	4334
OSTRICH	10	16812	444576.608	236184.521	16812	9455	7357	5126	5029	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
cvc5	0	14069	404207.163	411349.395	14069	14069	0	148	7721	489	0
2022-cvc5n	0	13853	453942.995	461410.672	13853	13853	0	364	7721	975	0
z3-alpha	0	13599	171340.306	170955.777	13599	13599	0	618	7721	802	0
OSTRICH Fixedn	0	9586	395576.734	204661.585	9586	9586	0	4631	7721	4990	0
Z3-Noodler Fixedn	0	7344	199311.53	199236.209	7344	7344	0	6873	7721	2042	4276
OSTRICH	1	9455	319989.546	159509.256	9455	9455	0	4762	7721	5029	0
Z3-Noodler	4	7405	187444.108	187450.515	7405	7405	0	6812	7721	1988	4334

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
cvc5	0	7377	89570.581	90083.348	7377	0	7377	227	14334	489	0
OSTRICH Fixedn	0	7356	124279.898	76297.815	7356	0	7356	248	14334	4990	0
z3-alpha	0	7298	8044.781	7974.585	7298	0	7298	306	14334	802	0
2022-cvc5n	0	7108	82469.426	82605.528	7108	0	7108	496	14334	975	0
Z3-Noodler Fixedn	1	5367	6155.031	6156.388	5367	0	5367	2237	14334	2042	4276
Z3-Noodler	1	5365	6202.083	6203.243	5365	0	5365	2239	14334	1988	4334
OSTRICH	9	7357	124587.061	76675.265	7357	0	7357	247	14334	5029	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
z3-alpha	0	19986	24673.627	24346.0	19986	12750	7236	1952	1814	0
cvc5	0	19837	11536.387	11324.357	19837	12774	7063	2101	2099	0
2022-cvc5n	0	19255	12926.94	12760.28	19255	12418	6837	2683	2681	0
OSTRICH Fixedn	0	15195	182021.615	68285.712	15195	8055	7140	6743	6742	0
Z3-Noodler Fixedn	1	12156	3482.216	3461.933	12156	6816	5340	9782	2690	4276
Z3-Noodler	5	12179	3359.219	3337.786	12179	6843	5336	9759	2606	4334
OSTRICH	9	15237	183465.374	68723.561	15237	8094	7143	6701	6683	0

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