QF_UFDT (Single Query Track)

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

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

Benchmarks: 203
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	cvc5

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	104	169813.755	169842.502	104	28	76	99	99	0
z3n	0	98	159924.689	159963.129	98	10	88	105	105	0
SMTInterpol	0	19	229500.84	228785.67	19	3	16	184	184	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	104	169831.325	169838.362	104	28	76	99	99	0
z3n	0	98	159938.689	159959.089	98	10	88	105	105	0
SMTInterpol	0	23	229865.65	228663.53	23	3	20	180	180	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	28	103106.401	103109.16	28	28	0	75	100	99	0
z3n	0	10	115844.323	115844.815	10	10	0	93	100	105	0
SMTInterpol	0	3	120001.068	120000.835	3	3	0	100	100	180	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	N/A	Timeout	Memout
z3n	0	88	44094.366	44114.274	88	0	88	12	103	105	0
cvc5	0	76	66724.924	66729.202	76	0	76	24	103	99	0
SMTInterpol	0	20	109864.582	108662.695	20	0	20	80	103	180	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
cvc5	0	3	4800.052	4800.05	3	3	0	200	200	0
z3n	0	3	4800.087	4800.087	3	3	0	200	200	0
SMTInterpol	0	3	4801.068	4800.835	3	3	0	200	200	0

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