toggle phases after restart (alternative of `Solver::rebuildOrderHeap`)

[shnarazk]

baseline

# 2017-08-31T16:03 /home/narazaki/.local/bin/mios-1.4.1 ; mios 1.4.1
"mios-1.4.1", 1, 200,    12.66
"mios-1.4.1", 2, 225,    42.70
"mios-1.4.1", 3, 250,    87.40
"mios-1.4.1", 4, "een",  5.13
"mios-1.4.1", 5, "bmc",  2.90
"mios-1.4.1", 6, "38b",  18.40

[shnarazk]

382b11d

# 2017-09-08T07:58 /home/narazaki/.local/bin/mios-WIP ; mios #master #clause-recycle
"mios-WIP", 1, 200,      29.92
"mios-WIP", 2, 225,      133.25
"mios-WIP", 3, 250,      killed after 1270.52
"mios-WIP", 4, "een",    4.67
"mios-WIP", 5, "bmc",    3.57
"mios-WIP", 6, "38b",    59.35

[shnarazk]

60b075d

# p='', t=1260 on xingu @ 2017-09-08T08:50:32+09:00
"mios-WIP", 1, 200,      11.53
"mios-WIP", 2, 225,      29.47
"mios-WIP", 3, 250,      91.94
"mios-WIP", 4, "een",    4.68
"mios-WIP", 5, "bmc",    4.66
"mios-WIP", 6, "38b",    13.15

[shnarazk]

FIY, this trick seems to work well.

By applying the following we got a similar result with Luby.

modified   src/SAT/Mios/Main.hs
@@ -780,7 +780,7 @@ solve s@Solver{..} assumps = do
         -- SOLVE:
         nc <- fromIntegral <$> nClauses s
-        let useLuby = False -- True
-            restart_inc = 1.75 :: Double
-            restart_first = 100 :: Double
+        let useLuby = True -- False -- True
+            restart_inc = 2.0 :: Double
+            restart_first = nc + fromIntegral nVars :: Double
             while' :: Double -> Double -> IO Bool
             while' nOfConflicts nOfLearnts = do

"mios-WIP", 1, 200,      13.48
"mios-WIP", 2, 225,      34.78
"mios-WIP", 3, 250,      156.92
"mios-WIP", 4, "een",    5.20
"mios-WIP", 5, "bmc",    3.45
"mios-WIP", 6, "38b",    8.29