QF_S (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OSTRICH Fixedn	0	8800	38043.704	23074.916	8800	5814	2986	47	47	0
OSTRICH	0	8798	35878.996	21386.873	8798	5812	2986	49	46	0
z3-alpha	0	8797	10373.323	10356.048	8797	5838	2959	50	33	0
2022-cvc5n	0	8794	30623.56	31066.1	8794	5837	2957	53	52	0
cvc5	0	8775	27096.927	28385.291	8775	5835	2940	72	68	4
Z3-Noodler	0	8711	8149.81	8136.353	8711	5741	2970	136	65	71
Z3-Noodler Fixedn	0	8710	6695.0	6685.942	8710	5740	2970	137	66	71

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
OSTRICH Fixedn	0	8800	38043.704	23074.916	8800	5814	2986	47	45	0
OSTRICH	0	8798	35878.996	21386.873	8798	5812	2986	49	45	0
z3-alpha	0	8797	10373.323	10356.048	8797	5838	2959	50	33	0
2022-cvc5n	0	8794	30623.56	31066.1	8794	5837	2957	53	52	0
cvc5	0	8775	27096.927	28385.291	8775	5835	2940	72	68	4
Z3-Noodler	0	8711	8149.81	8136.353	8711	5741	2970	136	65	71
Z3-Noodler Fixedn	0	8710	6695.0	6685.942	8710	5740	2970	137	66	71

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3-alpha	0	5838	5676.2	5659.94	5838	5838	0	13	2996	33	0
2022-cvc5n	0	5837	16436.966	16604.866	5837	5837	0	14	2996	52	0
cvc5	0	5835	8571.428	8613.21	5835	5835	0	16	2996	68	4
OSTRICH Fixedn	0	5814	27966.405	16354.065	5814	5814	0	37	2996	45	0
OSTRICH	0	5812	25787.55	14630.455	5812	5812	0	39	2996	45	0
Z3-Noodler	0	5741	4708.417	4701.164	5741	5741	0	110	2996	65	71
Z3-Noodler Fixedn	0	5740	3983.852	3976.405	5740	5740	0	111	2996	66	71

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
OSTRICH Fixedn	0	2986	10077.299	6720.85	2986	0	2986	4	5857	45	0
OSTRICH	0	2986	10091.446	6756.419	2986	0	2986	4	5857	45	0
Z3-Noodler Fixedn	0	2970	2711.148	2709.537	2970	0	2970	20	5857	66	71
Z3-Noodler	0	2970	3441.393	3435.188	2970	0	2970	20	5857	65	71
z3-alpha	0	2959	4697.123	4696.108	2959	0	2959	31	5857	33	0
2022-cvc5n	0	2957	14186.594	14461.233	2957	0	2957	33	5857	52	0
cvc5	0	2940	18525.499	19772.081	2940	0	2940	50	5857	68	4

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	8764	3612.196	3593.366	8764	5812	2952	83	83	0
OSTRICH	0	8747	26440.04	14234.621	8747	5771	2976	100	100	0
OSTRICH Fixedn	0	8744	26301.335	14110.924	8744	5768	2976	103	103	0
2022-cvc5n	0	8677	2045.367	2020.823	8677	5774	2903	170	170	0
cvc5	0	8674	1322.747	1302.688	8674	5799	2875	173	169	4
Z3-Noodler Fixedn	0	8663	1501.52	1491.312	8663	5717	2946	184	113	71
Z3-Noodler	0	8649	1534.285	1518.422	8649	5713	2936	198	127	71

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