QF_UFNIA (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

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

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24s Performance (parallel)
CVC4	CVC4	Yices2	CVC4	CVC4

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
CVC4	0	280	4956.472	4957.34	280	201	79	20		4	0
Yices2-fixedn	0	278	27012.633	27017.858	278	206	72	22		22	0
Yices2	0	278	27050.586	27019.621	278	206	72	22		22	0
2019-CVC4n	0	276	7447.503	7450.444	276	199	77	24		6	0
MathSAT5n	0	267	39792.185	39799.009	267	187	80	33		33	0
z3n	0	259	22582.889	22586.175	259	182	77	41		15	0
Alt-Ergo	0	39	7765.771	7468.795	39	0	39	261		6	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
CVC4	0	280	4957.312	4957.25	280	201	79	20		4	0
Yices2-fixedn	0	278	27016.013	27016.778	278	206	72	22		22	0
Yices2	0	278	27054.596	27018.621	278	206	72	22		22	0
2019-CVC4n	0	276	7449.963	7450.034	276	199	77	24		6	0
MathSAT5n	0	267	39798.665	39797.739	267	187	80	33		33	0
z3n	0	259	22585.009	22585.575	259	182	77	41		15	0
Alt-Ergo	0	39	7765.771	7468.795	39	0	39	261		6	0

SAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
Yices2-fixedn	0	206	1814.606	1815.054	206	206	0	94	22	0
Yices2	0	206	1853.228	1817.125	206	206	0	94	22	0
CVC4	0	201	2451.707	2451.663	201	201	0	99	4	0
2019-CVC4n	0	199	4899.391	4899.465	199	199	0	101	6	0
MathSAT5n	0	187	24135.714	24134.764	187	187	0	113	33	0
z3n	0	182	14205.962	14206.446	182	182	0	118	15	0
Alt-Ergo	0	0	7748.499	7462.34	0	0	0	300	6	0

UNSAT Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Timeout	Memout
MathSAT5n	0	80	9662.951	9662.975	80	0	80	220	33	0
CVC4	0	79	1209.573	1209.549	79	0	79	221	4	0
2019-CVC4n	0	77	2405.366	2405.371	77	0	77	223	6	0
z3n	0	77	4547.145	4547.218	77	0	77	223	15	0
Yices2	0	72	19201.367	19201.496	72	0	72	228	22	0
Yices2-fixedn	0	72	19201.407	19201.723	72	0	72	228	22	0
Alt-Ergo	0	39	15.675	5.939	39	0	39	261	6	0

24 seconds Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Solved UNSAT	Unsolved	Abstained	Timeout	Memout
CVC4	0	279	195.765	195.697	279	200	79	21		7	0
2019-CVC4n	0	275	254.862	254.935	275	198	77	25		9	0
Yices2	0	271	705.052	705.28	271	199	72	29		29	0
Yices2-fixedn	0	271	705.196	705.924	271	199	72	29		29	0
MathSAT5n	0	266	975.488	974.559	266	187	79	34		34	0
z3n	0	252	938.981	939.021	252	176	76	48		30	0
Alt-Ergo	0	39	252.597	196.448	39	0	39	261		7	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.