Bitvec (Single Query Track)

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

Page generated on 2022-08-10 11:17:44 +0000

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

Logics:

• BV : 970 benchmarks

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
cvc5	cvc5	cvc5	cvc5	Q3B

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	884	115396.641	106482.184	884	241	643	86	0	86	0
cvc5	0	854	159378.113	165480.205	854	231	623	116	0	116	0
Q3B	0	832	170169.933	166765.139	832	228	604	138	0	135	0
z3-4.8.17n	0	775	232309.365	232323.793	775	212	563	195	0	182	2
Bitwuzla	0	759	251975.775	251990.283	759	207	552	211	0	197	0
Q3B-pBDD	0	753	272789.717	270834.863	753	184	569	217	0	214	0
YicesQS	0	708	318217.125	318269.985	708	192	516	262	0	262	0
UltimateEliminator+MathSAT	0	304	206470.961	204316.516	304	27	277	666	0	137	22

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	894	126521.801	100383.777	894	244	650	76	0	76	0
cvc5	0	854	164783.792	165475.435	854	231	623	116	0	116	0
Q3B	0	835	173630.993	165779.923	835	228	607	135	0	132	0
z3-4.8.17n	0	775	232351.965	232315.743	775	212	563	195	0	182	2
Bitwuzla	0	759	252001.465	251982.573	759	207	552	211	0	197	0
Q3B-pBDD	0	754	272853.117	270065.62	754	184	570	216	0	213	0
YicesQS	0	708	318262.215	318260.635	708	192	516	262	0	262	0
UltimateEliminator+MathSAT	0	304	206554.511	204316.276	304	27	277	666	0	137	22

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	244	33317.726	22825.981	244	244	0	16	710	76	0
cvc5	0	231	52530.489	53074.316	231	231	0	29	710	116	0
Q3B	0	228	40705.429	39151.001	228	228	0	32	710	132	0
z3-4.8.17n	0	212	52689.537	52690.324	212	212	0	48	710	182	2
Bitwuzla	0	207	53987.651	53986.379	207	207	0	53	710	197	0
YicesQS	0	192	83158.836	83158.062	192	192	0	68	710	262	0
Q3B-pBDD	0	184	101080.024	100168.464	184	184	0	76	710	213	0
UltimateEliminator+MathSAT	0	27	121779.362	120767.225	27	27	0	233	710	137	22

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	650	62004.075	46357.796	650	0	650	34	286	76	0
cvc5	0	623	81053.304	81201.119	623	0	623	61	286	116	0
Q3B	0	607	101725.564	95428.922	607	0	607	77	286	132	0
Q3B-pBDD	0	570	140573.093	138697.156	570	0	570	114	286	213	0
z3-4.8.17n	0	563	148462.427	148425.418	563	0	563	121	286	182	2
Bitwuzla	0	552	166813.815	166796.194	552	0	552	132	286	197	0
YicesQS	0	516	203903.38	203902.573	516	0	516	168	286	262	0
UltimateEliminator+MathSAT	0	277	57132.971	55918.365	277	0	277	407	286	137	22

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
2019-Par4n	0	861	4683.684	3203.543	861	231	630	109	0	109	0
Q3B	0	802	5510.274	4597.963	802	210	592	168	0	167	0
z3-4.8.17n	0	738	5971.449	5970.704	738	207	531	232	0	230	2
Q3B-pBDD	0	715	7170.095	6616.71	715	155	560	255	0	254	0
cvc5	0	705	7313.725	7303.0	705	129	576	265	0	265	0
Bitwuzla	0	700	7040.545	7019.814	700	183	517	270	0	256	0
YicesQS	0	687	7014.644	7012.687	687	184	503	283	0	283	0
UltimateEliminator+MathSAT	0	290	9529.942	7741.171	290	20	270	680	0	182	22

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.