QF_Strings (Single Query Track)

Competition results for the QF_Strings division in the Single Query Track.

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

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

Logics:

• QF_S : 8847 benchmarks
• QF_SLIA : 21938 benchmarks
• QF_SNIA : 70 benchmarks

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	Abstained	Timeout	Memout
cvc5	0	30291	520876.164	529819.493	30291	19974	10317	564	0	557	4
2022-cvc5n	0	29825	567038.083	575084.373	29825	19760	10065	1030	0	1027	0
z3-alpha	0	29764	189759.852	189287.851	29764	19507	10257	1091	0	835	0
OSTRICH Fixedn	0	25786	518390.549	279618.422	25786	15444	10342	5069	0	5063	0
Z3-Noodler Fixedn	1	21421	212161.562	212078.539	21421	13084	8337	9364	70	2108	4347
Z3-Noodler	5	21482	202995.982	202990.131	21482	13147	8335	9303	70	2052	4405
OSTRICH	10	25670	468031.837	246482.979	25670	15327	10343	5185	0	5091	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	30291	520876.164	529819.493	30291	19974	10317	564	0	557	4
2022-cvc5n	0	29825	567038.083	575084.373	29825	19760	10065	1030	0	1027	0
z3-alpha	0	29764	189759.852	189287.851	29764	19507	10257	1091	0	835	0
OSTRICH Fixedn	0	25812	558107.459	304149.926	25812	15470	10342	5043	0	5035	0
Z3-Noodler Fixedn	1	21421	212161.562	212078.539	21421	13084	8337	9364	70	2108	4347
Z3-Noodler	5	21481	201796.002	201790.111	21481	13146	8335	9304	70	2053	4405
OSTRICH	10	25680	480650.027	257684.189	25680	15337	10343	5175	0	5074	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
cvc5	0	19974	412780.084	419964.064	19974	19974	0	164	10717	557	4
2022-cvc5n	0	19760	470382.063	478017.612	19760	19760	0	378	10717	1027	0
z3-alpha	0	19507	177017.948	176617.159	19507	19507	0	631	10717	835	0
OSTRICH Fixedn	0	15470	423750.262	221131.26	15470	15470	0	4668	10717	5035	0
Z3-Noodler Fixedn	0	13084	203295.382	203212.614	13084	13084	0	6984	10787	2108	4347
OSTRICH	1	15337	345971.52	174252.506	15337	15337	0	4801	10717	5074	0
Z3-Noodler	4	13146	192152.525	192151.68	13146	13146	0	6922	10787	2053	4405

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
OSTRICH Fixedn	0	10342	134357.197	83018.666	10342	0	10342	252	20261	5035	0
cvc5	0	10317	108096.08	109855.429	10317	0	10317	277	20261	557	4
z3-alpha	0	10257	12741.904	12670.692	10257	0	10257	337	20261	835	0
2022-cvc5n	0	10065	96656.02	97066.761	10065	0	10065	529	20261	1027	0
Z3-Noodler Fixedn	1	8337	8866.179	8865.925	8337	0	8337	2257	20261	2108	4347
Z3-Noodler	1	8335	9643.477	9638.432	8335	0	8335	2259	20261	2053	4405
OSTRICH	9	10343	134678.507	83431.684	10343	0	10343	251	20261	5074	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
z3-alpha	0	28820	28287.264	27940.808	28820	18632	10188	2035	0	1897	0
cvc5	0	28581	12860.626	12628.504	28581	18643	9938	2274	0	2268	4
2022-cvc5n	0	28002	14974.409	14783.176	28002	18262	9740	2853	0	2851	0
OSTRICH Fixedn	0	24009	208530.073	82512.246	24009	13893	10116	6846	0	6845	0
Z3-Noodler Fixedn	1	20819	4983.736	4953.244	20819	12533	8286	9966	70	2803	4347
Z3-Noodler	5	20828	4893.504	4856.207	20828	12556	8272	9957	70	2733	4405
OSTRICH	9	24054	210099.837	83070.977	24054	13935	10119	6801	0	6783	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.