Restarts

[akinanop]

This is a test issue :1234:

Restarts: Sometimes the search gets into the wrong direction, so it might be more efficient to restart solving. This technique implemented in all SAT solvers and will be useful here as well. The reasons for its success are quite interesting from a theoretical point of view: cf. Carla Gomes, Ryan Williams and Bart Selman: On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search, 2003, also see: http://www.cs.cornell.edu/gomes/TALKS/backdoors-UCLA05.pdf.

Inspiration/puzzle: In the n-queens problem the # of backtracks and solving times are not related to the number of clauses, which grows progressively (and quite excessively - each clause expresses two inequalities, see Examples).

Some preliminary numbers:

Queens	Backtracks	Time (sec)
60	-	timeout 1 hour
55	91	23
50	0	0
40	73	3
30	40	1
26	2	0
25	315	6
24	1796	12
23	0	0
22	127	1
21	115	0
20	0	0
19	956	3

[akinanop]

Discussion continued on mvl-solver-Wiki, restarts drastically improve search on certain inputs.

[akinanop]

Now there is a command line option for choosing a number of restarts. To see results of experiments with different number of restarts on n-queens problems go here: https://github.com/akinanop/mvl-solver/wiki/Restarts. @gsalzer