128bit sort key

[shnarazk]

• sortClauses didn't use activity correctly.
• A key use the 2 * Int64 (10-bit LBD + 50-bit Ac + 32-bit index) layout.

[shnarazk]

10L + 50A + 40I layout

▶️ clause activity should be used.

with the fixed scaleAct

"mios-66", 1, 200,       23.50
"mios-66", 2, 225,       54.28
"mios-66", 3, 250,       154.52
"mios-66", 4, "itox",    25.48
"mios-66", 5, "m283",    80.42
"mios-66", 6, "38b",     32.15
"mios-66", 7, "44b",     380.11

original (almost zero) scaleAct

"mios-66", 1, 200,       20.78
"mios-66", 2, 225,       52.81
"mios-66", 3, 250,       141.83 
"mios-66", 4, "itox",    26.91 !
"mios-66", 5, "m283",    113.16 !
"mios-66", 6, "38b",     41.49 !
"mios-66", 7, "44b",     509.94 !

without scaleAct. That means no activity.

"mios-66", 1, 200,       22.46
"mios-66", 2, 225,       53.11
"mios-66", 3, 250,       142.03
"mios-66", 4, "itox",    25.71
"mios-66", 5, "m283",    82.18 !
"mios-66", 6, "38b",     59.03 !
"mios-66", 7, "44b",     380.10

[shnarazk]

[shnarazk]

diff --git a/src/SAT/Mios/Main.hs b/src/SAT/Mios/Main.hs
index 0c5d3bf..4c74b8f 100644
--- a/src/SAT/Mios/Main.hs
+++ b/src/SAT/Mios/Main.hs
@@ -471,22 +471,22 @@ reduceDB s@Solver{..} = do
 --
 -- they are coded into an "Int64" as the following 62 bit layout:
 --
--- *  7 bits for rank (LBD)
--- * 33 bits for converted activity
+-- *  8 bits for rank (LBD)
+-- * 32 bits for converted activity
 -- * 22 bits for clauseVector index
 --
 rankWidth :: Int
-rankWidth = 7
+rankWidth = 8
 activityWidth :: Int
-activityWidth = 33              -- note: the maximum clause activity is 1e20.
+activityWidth = 32              -- note: the maximum clause activity is 1e20.
 indexWidth :: Int
-indexWidth = 22
+indexWidth = 22                 -- 4M
 rankMax :: Int
 rankMax = 2 ^ rankWidth - 1
 activityMax :: Int
 activityMax = 2 ^ activityWidth - 1
 indexMax :: Int
-indexMax = 2 ^ indexWidth - 1 -- 2^2 G = 4G
+indexMax = 2 ^ indexWidth - 1

 -- | sort clauses (good to bad) by using a 'proxy' @Vec Int64@ that holds weighted index.
 sortClauses :: Solver -> ClauseExtManager -> Int -> IO Int
@@ -499,10 +499,11 @@ sortClauses s cm limit' = do
   at <- (0.1 *) . (/ fromIntegral n) <$> get' (claInc s) -- activity threshold
   -- 1: assign keys
   let shiftLBD = activityWidth + indexWidth
+      am = fromIntegral activityMax :: Double
       scaleAct :: Double -> Int
       scaleAct x
         | x < 1e-20 = activityMax
-        | otherwise = activityMax * floor (1 - logBase 10 (x * 1e20) / 40)
+        | otherwise = floor $ am * (1 - logBase 10 (x * 1e20) / 40)
       assignKey :: Int -> Int -> IO Int
       assignKey ((< n) -> False) t = return t
       assignKey i t = do

2 Word (= 8+ 52 + 40 bit) layout and the bug fixed compact layout are very similar. To hold extensibility for future, 1.5.4 switched to 2 Word layout.