statcmp.md

Statistical comparison of the solvers

I run three sets of experiments via virtual.mwagent module. Then I parse the log using analyze_log.py and compute the statistical description of inference times using describe_infer_times.py. The boards used here can be found under example_boards/key. Here are the results.

On key board 1.csv

This is a Beginner board.

solver	mean	std	min	q25	median	q75	max
fullsat	0.00666667	0.000942809	0.006	0.006	0.006	0.007	0.008
mcdfs	0.00266667	0.000471405	0.002	0.0025	0.003	0.003	0.003
mcdfs_v100	0.004	0.00141421	0.003	0.003	0.003	0.0045	0.006
mcdfs_v500	0.00366667	0.000942809	0.003	0.003	0.003	0.004	0.005
mcdfs_nomc	0.003	0.000816497	0.002	0.0025	0.003	0.0035	0.004
mcsat	0.00433333	0.000942809	0.003	0.004	0.005	0.005	0.005
mcsat_v100	0.00466667	0.00124722	0.003	0.004	0.005	0.0055	0.006
mcsat_v500	0.00433333	0.000942809	0.003	0.004	0.005	0.005	0.005

On key board 2.csv

This is an Expert board.

solver	mean	std	min	q25	median	q75	max
fullsat	0.0141304	0.00213265	0.009	0.013	0.014	0.015	0.02
mcdfs	0.00852174	0.0025854	0.004	0.006	0.009	0.01	0.014
mcdfs_v100	0.00852174	0.00260217	0.004	0.006	0.009	0.01	0.014
mcdfs_v500	0.00830435	0.00249233	0.004	0.006	0.008	0.01	0.013
mcdfs_nomc	0.0083913	0.00242701	0.004	0.006	0.009	0.0095	0.013
mcsat	0.0086087	0.00224071	0.005	0.007	0.009	0.01	0.013
mcsat_v100	0.00865217	0.00221867	0.004	0.0065	0.009	0.0105	0.012
mcsat_v500	0.00865217	0.00199148	0.004	0.007	0.009	0.01	0.011

On key board 3.csv

This is an extra-large 40x80 board.

solver	mean	std	min	q25	median	q75	max
fullsat	0.292953	0.365448	0.04	0.04825	0.0795	0.5255	1.158
mcdfs	0.0405156	0.0242648	0.004	0.0315	0.04	0.043	0.185
mcdfs_v100	0.0447031	0.0346684	0.004	0.03175	0.041	0.045	0.231
mcdfs_v500	0.0432812	0.0324314	0.004	0.03225	0.041	0.043	0.217
mcdfs_nomc	0.0429531	0.0329974	0.005	0.03225	0.0405	0.043	0.223
mcsat	0.0343437	0.0145851	0.006	0.026	0.041	0.043	0.076
mcsat_v100	0.0344531	0.0157002	0.006	0.0265	0.041	0.044	0.091
mcsat_v500	0.0341562	0.0144819	0.005	0.02575	0.041	0.043	0.072

Conclusion

mcsatsolver is the best among the three.