exp. on reduction period

shnarazk · Sep 3, 2017 · 8232f99 · 8232f99
1 parent 5dfcb60
commit 8232f99
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/SAT/Mios/Main.hs b/src/SAT/Mios/Main.hs
@@ -757,11 +757,12 @@ solve s@Solver{..} assumps = do
         -- SOLVE:
         nc <- fromIntegral <$> nClauses s
         let
+          nv = fromIntegral nVars
           while :: Double -> Double -> IO Bool
           while nOfConflicts nOfLearnts = do
             status <- search s (floor nOfConflicts) (floor nOfLearnts)
             if status == lBottom
-              then while (1.5 * nOfConflicts) (2000 + nOfLearnts)
+              then while (1.4 * nOfConflicts) (nv + nOfLearnts)
               else cancelUntil s 0 >> return (status == lTrue)
         while 100 $ min (nc / 3.0) 10000