From 8db85da685192491d638c1b668d01efaa37e70b5 Mon Sep 17 00:00:00 2001 From: Oleg Grenrus Date: Wed, 24 Jul 2024 13:54:56 +0300 Subject: [PATCH 1/4] Add export lists to sat-simple-pure modules --- sat-simple-pure/Lifted.hs | 4 +++- sat-simple-pure/UnliftedSTRef.hs | 11 ++++++++--- sat-simple-pure/Vec.hs | 16 +++++++++------- 3 files changed, 20 insertions(+), 11 deletions(-) diff --git a/sat-simple-pure/Lifted.hs b/sat-simple-pure/Lifted.hs index cc17156..da2d6ad 100644 --- a/sat-simple-pure/Lifted.hs +++ b/sat-simple-pure/Lifted.hs @@ -1,4 +1,6 @@ -module Lifted where +module Lifted ( + Lifted (..), +) where import Data.Kind (Type) import GHC.Exts (UnliftedType) diff --git a/sat-simple-pure/UnliftedSTRef.hs b/sat-simple-pure/UnliftedSTRef.hs index 00fd4ae..7c27cac 100644 --- a/sat-simple-pure/UnliftedSTRef.hs +++ b/sat-simple-pure/UnliftedSTRef.hs @@ -1,6 +1,11 @@ {-# LANGUAGE MagicHash #-} {-# LANGUAGE UnboxedTuples #-} -module UnliftedSTRef where +module UnliftedSTRef ( + USTRef, + newUSTRef, + readUSTRef, + writeUSTRef, +) where import Data.Kind (Type) import GHC.Exts (MutVar#, UnliftedType, newMutVar#, readMutVar#, writeMutVar#) @@ -12,8 +17,8 @@ type USTRef :: Type -> UnliftedType -> Type data USTRef s a = USTRef (MutVar# s a) newUSTRef :: a -> ST s (USTRef s a) -newUSTRef init = ST $ \s1# -> - case newMutVar# init s1# of { (# s2#, var# #) -> +newUSTRef x = ST $ \s1# -> + case newMutVar# x s1# of { (# s2#, var# #) -> (# s2#, USTRef var# #) } readUSTRef :: USTRef s a -> ST s (Lifted a) diff --git a/sat-simple-pure/Vec.hs b/sat-simple-pure/Vec.hs index 318db9c..98ee30a 100644 --- a/sat-simple-pure/Vec.hs +++ b/sat-simple-pure/Vec.hs @@ -1,4 +1,12 @@ -module Vec where +module Vec ( + Vec, + newVec, + sizeofVec, + insertVec, + readVec, + writeVec, + shrinkVec, +) where import Control.Monad (forM_) import Control.Monad.ST (ST) @@ -50,12 +58,6 @@ readVec (Vec _ arr) i = readArray arr i writeVec :: Vec s a -> Int -> a -> ST s () writeVec (Vec _ arr) i x = writeArray arr i x -clearVec :: Vec s a -> ST s () -clearVec (Vec sizeRef arr) = do - size <- readSTRef sizeRef - forM_ [0 .. size - 1] $ \i -> writeArray arr i unused - writeSTRef sizeRef 0 - -- | Shrink vector. New size should be smaller than the current. shrinkVec :: Vec s a -> Int -> ST s () shrinkVec (Vec sizeRef arr) newSize = do From a8a57bcd2276076954b42fea691ba44720baf3af Mon Sep 17 00:00:00 2001 From: Oleg Grenrus Date: Wed, 24 Jul 2024 14:00:54 +0300 Subject: [PATCH 2/4] Use PrimVar in Vec --- sat-simple-pure/Vec.hs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/sat-simple-pure/Vec.hs b/sat-simple-pure/Vec.hs index 98ee30a..4e214db 100644 --- a/sat-simple-pure/Vec.hs +++ b/sat-simple-pure/Vec.hs @@ -10,25 +10,25 @@ module Vec ( import Control.Monad (forM_) import Control.Monad.ST (ST) -import Data.STRef import Data.Primitive.Array +import Data.Primitive.PrimVar import Unsafe.Coerce (unsafeCoerce) -data Vec s a = Vec {-# UNPACK #-} !(STRef s Int) {-# UNPACK #-} !(MutableArray s a) +data Vec s a = Vec {-# UNPACK #-} !(PrimVar s Int) {-# UNPACK #-} !(MutableArray s a) newVec :: Int -- ^ capacity -> ST s (Vec s a) newVec capacity = do arr <- newArray capacity unused - size <- newSTRef 0 + size <- newPrimVar 0 return (Vec size arr) unused :: a unused = unsafeCoerce () sizeofVec :: Vec s a -> ST s Int -sizeofVec (Vec size _) = readSTRef size +sizeofVec (Vec size _) = readPrimVar size -- | Insert at the end: @push_back@ -- @@ -37,19 +37,19 @@ sizeofVec (Vec size _) = readSTRef size -- so we don't need an extra STRef. insertVec :: Vec s a -> a -> ST s (Vec s a) insertVec vec@(Vec sizeRef arr) x = do - size <- readSTRef sizeRef + size <- readPrimVar sizeRef let !capacity = sizeofMutableArray arr if size < capacity then do writeArray arr size x - writeSTRef sizeRef (size + 1) + writePrimVar sizeRef (size + 1) return vec else do new <- newArray (capacity * 2) unused copyMutableArray new 0 arr 0 size writeArray new size x - writeSTRef sizeRef (size + 1) + writePrimVar sizeRef (size + 1) return (Vec sizeRef new) readVec :: Vec s a -> Int -> ST s a @@ -61,6 +61,6 @@ writeVec (Vec _ arr) i x = writeArray arr i x -- | Shrink vector. New size should be smaller than the current. shrinkVec :: Vec s a -> Int -> ST s () shrinkVec (Vec sizeRef arr) newSize = do - size <- readSTRef sizeRef + size <- readPrimVar sizeRef forM_ [newSize .. size - 1] $ \i -> writeArray arr i unused - writeSTRef sizeRef newSize + writePrimVar sizeRef newSize From c66d1ef6cafb646cae2f064c69cccb6c2adfa371 Mon Sep 17 00:00:00 2001 From: Oleg Grenrus Date: Wed, 24 Jul 2024 14:25:32 +0300 Subject: [PATCH 3/4] Add SparseSet structure --- sat-simple-pure/SparseSet.hs | 102 +++++++++++++++++++++++++++++++++++ spdx.cabal | 1 + 2 files changed, 103 insertions(+) create mode 100644 sat-simple-pure/SparseSet.hs diff --git a/sat-simple-pure/SparseSet.hs b/sat-simple-pure/SparseSet.hs new file mode 100644 index 0000000..10a5bd7 --- /dev/null +++ b/sat-simple-pure/SparseSet.hs @@ -0,0 +1,102 @@ +module SparseSet ( + SparseSet, + newSparseSet, + memberSparseSet, + insertSparseSet, + popSparseSet, + elemsSparseSet, +) where + +import Control.Monad.ST (ST) +import Data.Primitive.PrimArray +import Data.Primitive.PrimVar + +-- $setup +-- >>> import Control.Monad.ST (runST) + +-- | https://research.swtch.com/sparse +-- +-- An 'Int' set which support efficient popping ('popSparseSet'). +data SparseSet s = SS (PrimVar s Int) (MutablePrimArray s Int) (MutablePrimArray s Int) + +-- | Create new sparse set +-- +-- >>> runST $ newSparseSet 100 >>= elemsSparseSet +-- [] +newSparseSet + :: Int -- ^ max integer + -> ST s (SparseSet s) +newSparseSet capacity = do + size <- newPrimVar 0 + dense <- newPrimArray capacity + sparse <- newPrimArray capacity + return (SS size dense sparse) + +-- | Test for membership +-- +-- >>> runST $ do { set <- newSparseSet 100; mapM_ (insertSparseSet set) [3,5,7,11,13,11]; memberSparseSet set 10 } +-- False +-- +-- >>> runST $ do { set <- newSparseSet 100; mapM_ (insertSparseSet set) [3,5,7,11,13,11]; memberSparseSet set 13 } +-- True +-- +memberSparseSet :: SparseSet s -> Int -> ST s Bool +memberSparseSet (SS size dense sparse) x = do + n <- readPrimVar size + i <- readPrimArray sparse x + if i < n + then do + x' <- readPrimArray dense i + return (x' == x) + else return False + +-- | Insert into set +-- +-- >>> runST $ do { set <- newSparseSet 100; mapM_ (insertSparseSet set) [3,5,7,11,13,11]; elemsSparseSet set } +-- [13,11,7,5,3] +-- +insertSparseSet :: SparseSet s -> Int -> ST s () +insertSparseSet (SS size dense sparse) x = do + n <- readPrimVar size + i <- readPrimArray sparse x + if i < n + then do + x' <- readPrimArray dense i + if x == x' then return () else insert n + else insert n + where + insert n = do + writePrimArray dense n x + writePrimArray sparse x n + writePrimVar size (n + 1) + +-- | Pop element from the set +-- +-- >>> runST $ do { set <- newSparseSet 100; mapM_ (insertSparseSet set) [3,5,7,11,13,11]; popSparseSet set } +-- Just 13 +-- +popSparseSet :: SparseSet s -> ST s (Maybe Int) +popSparseSet (SS size dense _sparse) = do + n <- readPrimVar size + if n <= 0 + then return Nothing + else do + let !n' = n - 1 + i <- readPrimArray dense n' + writePrimVar size n' + return (Just i) + +-- | Elements of the set +elemsSparseSet :: SparseSet s -> ST s [Int] +elemsSparseSet (SS size dense _sparse) = do + n <- readPrimVar size + go [] 0 n + where + go !acc !i !n + | i < n + = do + x <- readPrimArray dense i + go (x : acc) (i + 1) n + + | otherwise + = return acc \ No newline at end of file diff --git a/spdx.cabal b/spdx.cabal index 4ff6d79..235e4af 100644 --- a/spdx.cabal +++ b/spdx.cabal @@ -63,6 +63,7 @@ library sat-simple-pure DPLL EST Lifted + SparseSet UnliftedSTRef Vec From 5c221b48f5e4a780e4fce79d154cd39e43f030c8 Mon Sep 17 00:00:00 2001 From: Oleg Grenrus Date: Wed, 24 Jul 2024 14:41:08 +0300 Subject: [PATCH 4/4] Use SparseSet for unit literals set --- sat-simple-pure/DPLL.hs | 123 +++++++++++++++++++---------------- sat-simple-pure/EST.hs | 4 +- sat-simple-pure/SparseSet.hs | 18 +++-- sat-simple-pure/Vec.hs | 6 +- 4 files changed, 85 insertions(+), 66 deletions(-) diff --git a/sat-simple-pure/DPLL.hs b/sat-simple-pure/DPLL.hs index 7ad98cd..c022d98 100644 --- a/sat-simple-pure/DPLL.hs +++ b/sat-simple-pure/DPLL.hs @@ -21,6 +21,7 @@ module DPLL ( import Control.Monad.ST (ST) import Data.Bits (complementBit, testBit, unsafeShiftL, unsafeShiftR) +import Data.Coerce (coerce) import Data.Functor ((<&>)) import Data.IntSet (IntSet) import Data.Primitive.PrimArray (PrimArray, indexPrimArray, primArrayFromList, sizeofPrimArray) @@ -33,6 +34,7 @@ import Data.Primitive.ByteArray resizeMutableByteArray, shrinkMutableByteArray, writeByteArray) import Lifted +import SparseSet import UnliftedSTRef #ifdef TWO_WATCHED_LITERALS @@ -159,18 +161,21 @@ minViewVarSet (VS xs) = case IntSet.minView xs of -- LitSet ------------------------------------------------------------------------------- -newtype LitSet = LS IntSet +newtype LitSet s = LS (SparseSet s) -emptyLitSet :: LitSet -emptyLitSet = LS IntSet.empty +newLitSet :: Int -> ST s (LitSet s) +newLitSet n = LS <$> newSparseSet n -insertLitSet :: Lit -> LitSet -> LitSet -insertLitSet (MkLit l) (LS ls) = LS (IntSet.insert l ls) +insertLitSet :: Lit -> LitSet s -> ST s () +insertLitSet (MkLit l) (LS ls) = insertSparseSet ls l -minViewLitSet :: LitSet -> Maybe (Lit, LitSet) -minViewLitSet (LS xs) = case IntSet.minView xs of - Nothing -> Nothing - Just (x, xs') -> Just (MkLit x, LS xs') +minViewLitSet :: LitSet s -> ST s (Maybe Lit) +minViewLitSet (LS xs) = do + x <- popSparseSet xs + return (coerce x) + +clearLitSet :: LitSet s -> ST s () +clearLitSet (LS xs) = clearSparseSet xs ------------------------------------------------------------------------------- -- Clauses @@ -404,8 +409,10 @@ solve solver@Solver {..} = whenOk_ (simplify solver) $ do vars <- readSTRef variables -- traceM $ "solve " ++ show (length clauses') -#ifdef TWO_WATCHED_LITERALS litCount <- readSTRef nextLit + units <- newLitSet litCount + +#ifdef TWO_WATCHED_LITERALS clauseDB <- newClauseDB litCount forM_ clauses' $ \c -> satisfied2_ solution c >>= \case Unresolved_ l1 l2 -> insertClauseDB l1 l2 c clauseDB @@ -414,32 +421,32 @@ solve solver@Solver {..} = whenOk_ (simplify solver) $ do let clauseDB = clauses' #endif - solveLoop clauseDB End emptyLitSet solution vars >>= \case + solveLoop clauseDB End units solution vars >>= \case False -> conflict solver True -> return True -solveLoop :: ClauseDB s -> Trail -> LitSet -> PartialAssignment s -> VarSet -> ST s Bool -solveLoop !clauseDb !trail !units !pa !vars - | Just (l, units') <- minViewLitSet units - = lookupPartialAssignment l pa >>= \case - LUndef -> do - insertPartialAssignment l pa - let !vars' = deleteVarSet (litToVar l) vars - unitPropagate l clauseDb (Deduced l trail) units pa vars' - LTrue -> solveLoop clauseDb trail units' pa vars - LFalse -> backtrack clauseDb trail pa vars - - | Just (v, vars') <- minViewVarSet vars - = do - -- traceM $ "decide" ++ show v - let l = varToLit v - insertPartialAssignment l pa - unitPropagate l clauseDb (Decided l trail) emptyLitSet pa vars' - - | otherwise - = return True - -unitPropagate :: forall s. Lit -> ClauseDB s -> Trail -> LitSet -> PartialAssignment s -> VarSet -> ST s Bool +solveLoop :: ClauseDB s -> Trail -> LitSet s -> PartialAssignment s -> VarSet -> ST s Bool +solveLoop !clauseDb !trail !units !pa !vars = do + minViewLitSet units >>= \case + Just l -> lookupPartialAssignment l pa >>= \case + LUndef -> do + insertPartialAssignment l pa + let !vars' = deleteVarSet (litToVar l) vars + unitPropagate l clauseDb (Deduced l trail) units pa vars' + LTrue -> solveLoop clauseDb trail units pa vars + LFalse -> backtrack clauseDb trail units pa vars + Nothing + | Just (v, vars') <- minViewVarSet vars + -> do + -- traceM $ "decide" ++ show v + let l = varToLit v + insertPartialAssignment l pa + unitPropagate l clauseDb (Decided l trail) units pa vars' + + | otherwise + -> return True + +unitPropagate :: forall s. Lit -> ClauseDB s -> Trail -> LitSet s -> PartialAssignment s -> VarSet -> ST s Bool #ifdef TWO_WATCHED_LITERALS @@ -448,14 +455,14 @@ unitPropagate !l !clauseDb !trail !units !pa !vars = do -- traceM $ "unitPropagate " ++ show (l, dbSize) watches <- lookupClauseDB (neg l) clauseDb size <- sizeofVec watches - go units watches 0 0 size + go watches 0 0 size where - go :: LitSet -> Vec s Watch -> Int -> Int -> Int -> ST s Bool - go !us watches i j size + go :: Vec s Watch -> Int -> Int -> Int -> ST s Bool + go watches i j size | i >= size = do shrinkVec watches j - solveLoop clauseDb trail us pa vars + solveLoop clauseDb trail units pa vars | otherwise = readVec watches i >>= \ w@(W l' c) -> satisfied2_ pa c >>= \case @@ -473,49 +480,53 @@ unitPropagate !l !clauseDb !trail !units !pa !vars = do copy (i + 1) (j + 1) - backtrack clauseDb trail pa vars + backtrack clauseDb trail units pa vars Satisfied_ -> do writeVec watches j w - go us watches (i + 1) (j + 1) size + go watches (i + 1) (j + 1) size Unit_ u -> do writeVec watches j w - go (insertLitSet u us) watches (i + 1) (j + 1) size + insertLitSet u units + go watches (i + 1) (j + 1) size Unresolved_ l1 l2 | l2 /= l', l2 /= l -> do insertWatch l2 w clauseDb - go us watches (i + 1) j size + go watches (i + 1) j size | l1 /= l', l1 /= l -> do insertWatch l1 w clauseDb - go us watches (i + 1) j size + go watches (i + 1) j size | otherwise -> error ("watch" ++ show (l, l1, l2, l')) #else -unitPropagate !_ !clauseDb !trail !units !pa !vars = go units clauseDb +unitPropagate !_ !clauseDb !trail !units !pa !vars = go clauseDb where - go :: LitSet -> [Clause2] -> ST s Bool - go us [] = solveLoop clauseDb trail us pa vars - go us (c:cs) = satisfied2_ pa c >>= \case - Conflicting_ -> backtrack clauseDb trail pa vars - Satisfied_ -> go us cs - Unit_ u -> go (insertLitSet u us) cs - Unresolved_ _ _ -> go us cs + go :: [Clause2] -> ST s Bool + go [] = solveLoop clauseDb trail units pa vars + go (c:cs) = satisfied2_ pa c >>= \case + Conflicting_ -> backtrack clauseDb trail units pa vars + Satisfied_ -> go cs + Unit_ u -> do + insertLitSet u units + go cs + Unresolved_ _ _ -> go cs #endif -backtrack :: ClauseDB s -> Trail -> PartialAssignment s -> VarSet -> ST s Bool -backtrack !_clauseDb End !_pa !_vars = return False -backtrack clauseDb (Deduced l trail) pa vars = do +backtrack :: ClauseDB s -> Trail -> LitSet s -> PartialAssignment s -> VarSet -> ST s Bool +backtrack !_clauseDb End !_units !_pa !_vars = return False +backtrack clauseDb (Deduced l trail) units pa vars = do deletePartialAssignment l pa - backtrack clauseDb trail pa (insertVarSet (litToVar l) vars) -backtrack clauseDb (Decided l trail) pa vars = do + backtrack clauseDb trail units pa (insertVarSet (litToVar l) vars) +backtrack clauseDb (Decided l trail) units pa vars = do deletePartialAssignment l pa insertPartialAssignment (neg l) pa - unitPropagate (neg l) clauseDb (Deduced (neg l) trail) emptyLitSet pa vars + clearLitSet units + unitPropagate (neg l) clauseDb (Deduced (neg l) trail) units pa vars ------------------------------------------------------------------------------- -- simplify diff --git a/sat-simple-pure/EST.hs b/sat-simple-pure/EST.hs index 007bea8..e51ef6b 100644 --- a/sat-simple-pure/EST.hs +++ b/sat-simple-pure/EST.hs @@ -11,9 +11,7 @@ module EST ( earlyExitEST, ) where -import GHC.Exts - (PromptTag#, State#, control0#, newPromptTag#, oneShot, prompt#, runRW#, - unsafeCoerce#) +import GHC.Exts (PromptTag#, State#, control0#, newPromptTag#, oneShot, prompt#, runRW#, unsafeCoerce#) import GHC.ST (ST (..)) control0## diff --git a/sat-simple-pure/SparseSet.hs b/sat-simple-pure/SparseSet.hs index 10a5bd7..35b2082 100644 --- a/sat-simple-pure/SparseSet.hs +++ b/sat-simple-pure/SparseSet.hs @@ -5,9 +5,10 @@ module SparseSet ( insertSparseSet, popSparseSet, elemsSparseSet, + clearSparseSet, ) where -import Control.Monad.ST (ST) +import Control.Monad.ST (ST) import Data.Primitive.PrimArray import Data.Primitive.PrimVar @@ -70,7 +71,7 @@ insertSparseSet (SS size dense sparse) x = do writePrimArray sparse x n writePrimVar size (n + 1) --- | Pop element from the set +-- | Pop element from the set. -- -- >>> runST $ do { set <- newSparseSet 100; mapM_ (insertSparseSet set) [3,5,7,11,13,11]; popSparseSet set } -- Just 13 @@ -86,6 +87,15 @@ popSparseSet (SS size dense _sparse) = do writePrimVar size n' return (Just i) +-- | Clear sparse set. +-- +-- >>> runST $ do { set <- newSparseSet 100; mapM_ (insertSparseSet set) [3,5,7,11,13,11]; clearSparseSet set; elemsSparseSet set } +-- [] +-- +clearSparseSet :: SparseSet s -> ST s () +clearSparseSet (SS size _ _) = do + writePrimVar size 0 + -- | Elements of the set elemsSparseSet :: SparseSet s -> ST s [Int] elemsSparseSet (SS size dense _sparse) = do @@ -97,6 +107,6 @@ elemsSparseSet (SS size dense _sparse) = do = do x <- readPrimArray dense i go (x : acc) (i + 1) n - + | otherwise - = return acc \ No newline at end of file + = return acc diff --git a/sat-simple-pure/Vec.hs b/sat-simple-pure/Vec.hs index 4e214db..45b8ef6 100644 --- a/sat-simple-pure/Vec.hs +++ b/sat-simple-pure/Vec.hs @@ -8,11 +8,11 @@ module Vec ( shrinkVec, ) where -import Control.Monad (forM_) -import Control.Monad.ST (ST) +import Control.Monad (forM_) +import Control.Monad.ST (ST) import Data.Primitive.Array import Data.Primitive.PrimVar -import Unsafe.Coerce (unsafeCoerce) +import Unsafe.Coerce (unsafeCoerce) data Vec s a = Vec {-# UNPACK #-} !(PrimVar s Int) {-# UNPACK #-} !(MutableArray s a)