Armin’s Rapid restart strategy
After taking a look at Armin’s invited talk slides at the SAT 07 conference, I decided to give a try to the rapid restart strategy mentioned by Armin.
I implemented the notion of RestartStrategy in SAT4J.
The default option is the one from MiniSAT (the initial number of conflict is 100, that number is increased by a factor of 1.5 at each restart).
public class MiniSATRestarts implements RestartStrategy { private double nofConflicts; private SearchParams params; public void init(SearchParams params) { this.params = params; nofConflicts = params.getInitConflictBound(); } public long nextRestartNumberOfConflict() { return Math.round(nofConflicts); } public void onRestart() { nofConflicts *= params.getConflictBoundIncFactor(); } @Override public String toString() { return "MiniSAT restarts strategy"; } }
A new option is Armin scheme.
public class ArminRestarts implements RestartStrategy { private double inner,outer; private long conflicts; private SearchParams params; public void init(SearchParams params) { this.params = params; inner = params.getInitConflictBound(); outer = params.getInitConflictBound(); conflicts = Math.round(inner); } public long nextRestartNumberOfConflict() { return conflicts; } public void onRestart() { if (inner>=outer) { outer *= params.getConflictBoundIncFactor(); inner = params.getInitConflictBound(); } else { inner *= params.getConflictBoundIncFactor(); } conflicts = Math.round(inner); } @Override public String toString() { return "Armin Biere (Picosat) restarts strategy"; } }
Another one is the Luby suite as proposed in Henry Kautz SATZ_rand and used recently in Tinisat and RSAT.
public class LubyRestarts implements RestartStrategy { // taken from SATZ_rand source code static final long luby_super(long i) { long power; long k; assert i > 0; /* let 2^k be the least power of 2 >= (i+1) */ k = 1; power = 2; while (power < (i + 1)) { k += 1; power *= 2; } if (power == (i + 1)) return (power / 2); return (luby_super(i - (power / 2) + 1)); } private int factor; private int count; public LubyRestarts() { setFactor(32); // uses TiniSAT default } public void setFactor(int factor) { this.factor = factor; } public int getFactor() { return factor; } public void init(SearchParams params) { count = 1; } public long nextRestartNumberOfConflict() { return luby_super(count)*factor; } public void onRestart() { count++; } @Override public String toString() { return "luby style (SATZ_rand, TiniSAT) restarts strategy with factor "+factor; } }
Using the SAT Race 2006 benchmarks set (100 benchmarks), with a timeout of 900 seconds per benchmark, I got the following results:
- MiniSAT scheme: 58 (29 SAT / 29 UNSAT) benchmarks solved in 835mn
- Luby scheme (factor 32): 59 (24 SAT / 35 UNSAT) benchmarks solved in 790mn
- Luby scheme (factor 512, without Rsat phase caching,without reason simplification): 48 (19 SAT / 29 UNSAT) benchmarks solved in 947mn
- Luby scheme (factor 512, with Rsat phase caching,without reason simplification): 55 (26 SAT/29 UNSAT) benchmarks solved in 866mn
- Luby scheme (factor 512, all options enabled): 61 (29 SAT /32 UNSAT) benchmarks solved in 788mn
- Armin scheme: 61 (27 SAT / 34 UNSAT) benchmarks solved in 790mn.
Note that I implemented the RSat phase saving some weeks ago: according to Armin, the rapid restart scheme only works with that phase saving scheme. The phase saving feature alone allowed SAT4J to jump from 52 to 58 benchmarks solved. If you haven’t tried that feature yet, you should take a look at it 
Loading ...
RSat uses the Luby scheme with unit step=512. I think TiniSat does this as well.
You may want to try this on your solver. In my experience, 512 is quite a bit better than 32.
Also, I think Armin claimed that this technique is better with UNSAT instances. I have never checked this out. This might be something interesting to see.
Comment by knot — June 12, 2007 @ 9:33 pm
Knot, I updated my post with the SAT/UNSAT numbers.
I am currently running SAT4J on the very same benchmarks with a Luby factor of 512. It looks like the results will be worst than all the other options (46 benchmarks solved among 96 benchmarks).
[Update] My mistake. The Rsat phase caching was not enabled. I am rerunning the solver with the correct configuration.
[Update 2] The reason simplification from MiniSAT 1.14 was not activated either
I need to rerun everything. I run it on my home computer that is very similar to Armin’s cluster nodes so it takes roughly 12 hours or so to have the results.
Comment by Daniel Le Berre — June 13, 2007 @ 1:55 pm
The point in the talk regarding using restarts for unsat instances was
are a good
that even for unsat instances restarts are really important, since
switching them off completely would result in only 48 instances solved
out of 78 picosat would solve otherwise (from the 100 SAT Race instances).
It does not mean that rapid restarts (aka Armin restarts
idea for unsat instances. Note that picosat was not really fast on UNSAT instances.
That could either be due to not using a pre-processor or because of the
rapid restarts. I just do not know. This is a good question for
an experimental analysis. BTW, after fixing our cluster last week I ran
the same picosat again, now with just phase saving switched off. Then
picosat can solve 61 instances. So clearly rapid restarts and phase
saving both give improvements independently, but it is not clear whether
one is necessary for the other (I would need to run the examples with
both options turned off, but the cluster is now occupied), even though
it is my intuition.
Comment by armin — June 13, 2007 @ 3:17 pm
Knot,
Using a Luby factor of 512 does improve the behavior of the solver: 61 benchmarks solved, same as Armin’s scheme (but different benchs solved).
Comment by Daniel Le Berre — June 15, 2007 @ 9:09 pm
Thank you for the information.
In my experience, the difference between different units is not that significant, but again 512 seems to be a local maximum.
Comment by knot — June 16, 2007 @ 8:50 am