foo

.stylish-haskell.yaml

@@ -9,7 +9,7 @@ steps:
       style: vertical
       remove_redundant: true
   - trailing_whitespace: {}
-columns: 80
+columns: 120
 language_extensions:
   - DataKinds
   - EmptyCase

CHANGELOG.md

@@ -2,6 +2,9 @@
 
 - Support GHC-8.6.5...9.10.1
 - Use better algorithm for expression equivalence and preorder
+  (It's still very slow compared to the state of the art SAT solvers:
+   it cannot solve the sudoku example in reasonable time;
+   but it's still a lot faster than the naive algorithm used previously)
 - Remove "Distribution.SPDX.Extra.Internal" module
 
 1

cabal.project

@@ -1,4 +1,7 @@
 packages: .
 tests: True
 
+package spdx
+  ghc-options: -Wall
+
 -- cabal run test -- -p "LicenseEx" --quickcheck-tests 1000 --quickcheck-timeout=1s --quickcheck-replay="(SMGen 5177394945948384830 10312189237211584183,97)"

examples/sat-simple-sudoku.hs

@@ -10,6 +10,7 @@ import Control.Applicative    (liftA2)
 import Control.Monad          (when)
 import Control.Monad.IO.Class (liftIO)
 import Data.Foldable          (for_, toList, traverse_)
+import System.Exit (exitSuccess, exitFailure)
 
 import Control.Monad.SAT
 
@@ -52,7 +53,14 @@ main = do
         Nothing -> putStrLn "No solution"
         Just sol -> do
             putStrLn "Solution:"
-            putStr $ render $ decode sol
+            let solution' = decode sol
+            putStr $ render solution'
+
+            if solution' == solution
+            then exitSuccess
+            else do
+                putStrLn "Doesn't match solution"
+                exitFailure
 
 -------------------------------------------------------------------------------
 -- Initial values
@@ -62,6 +70,8 @@ initValues :: Nine (Nine Int)
 initValues = N9
     -- From https://en.wikipedia.org/w/index.php?title=Sudoku&oldid=543290082
 
+    -- We make the problem easier, though DPLL can solve this sudoku given enough time (i.e. minutes).
+
     (N9 5 3 4 6 7 8 9 1 2)
     (N9 6 7 2 1 9 5 3 4 8)
     (N9 1 9 8 3 4 2 5 6 7)
@@ -86,6 +96,18 @@ initValues = N9
     (N9 0 0 0 4 1 9 0 0 5)
     (N9 0 0 0 0 8 0 0 7 9)
 
+solution :: Nine (Nine Int)
+solution = N9
+    (N9 5 3 4 6 7 8 9 1 2)
+    (N9 6 7 2 1 9 5 3 4 8)
+    (N9 1 9 8 3 4 2 5 6 7)
+    (N9 8 5 9 7 6 1 4 2 3)
+    (N9 4 2 6 8 5 3 7 9 1)
+    (N9 7 1 3 9 2 4 8 5 6)
+    (N9 9 6 1 5 3 7 2 8 4)
+    (N9 2 8 7 4 1 9 6 3 5)
+    (N9 3 4 5 2 8 6 1 7 9)
+
 -------------------------------------------------------------------------------
 -- Rendering
 -------------------------------------------------------------------------------
@@ -114,14 +136,14 @@ renderGroups begin middle end (N (T xs ys zs)) =
 -------------------------------------------------------------------------------
 
 data Triple a = T a a a
-  deriving (Functor, Foldable, Traversable)
+  deriving (Eq, Functor, Foldable, Traversable)
 
 instance Applicative Triple where
     pure x = T x x x
     T f g h <*> T x y z = T (f x) (g y) (h z)
 
 newtype Nine a = N { unN :: Triple (Triple a) }
-  deriving (Functor, Foldable, Traversable)
+  deriving (Eq, Functor, Foldable, Traversable)
 
 instance Applicative Nine where
     pure x = N (pure (pure x))

sat-simple-pure/DPLL.hs

@@ -5,7 +5,6 @@
 {-# LANGUAGE MagicHash                  #-}
 {-# LANGUAGE RecordWildCards            #-}
 {-# LANGUAGE StandaloneDeriving         #-}
-{-# OPTIONS_GHC -Wall #-}
 module DPLL (
     Solver,
     newSolver,
@@ -18,26 +17,28 @@ module DPLL (
     modelValue,
 ) where
 
--- This is buggy
--- #define TWO_WATCHED_LITERALS
+#define TWO_WATCHED_LITERALS
 
 import Control.Monad.ST         (ST)
-import Data.Bits
+import Data.Bits                (complementBit, testBit, unsafeShiftL, unsafeShiftR)
 import Data.Functor             ((<&>))
 import Data.IntSet              (IntSet)
-import Data.Primitive.ByteArray
-import Data.Primitive.PrimArray
+import Data.Primitive.PrimArray (PrimArray, indexPrimArray, primArrayFromList, sizeofPrimArray)
 import Data.Primitive.Types     (Prim)
-import Data.STRef
+import Data.STRef               (STRef, modifySTRef, newSTRef, readSTRef, writeSTRef)
 import Data.Word                (Word8)
 
+import Data.Primitive.ByteArray
+       (MutableByteArray (..), MutableByteArray#, getSizeofMutableByteArray, newByteArray, readByteArray,
+       resizeMutableByteArray, shrinkMutableByteArray, writeByteArray)
+
 import Lifted
 import UnliftedSTRef
 
 #ifdef TWO_WATCHED_LITERALS
+import Control.Monad        (forM_)
+import Data.Primitive.Array (MutableArray, newArray, readArray, sizeofMutableArray, writeArray)
 import Vec
-import Control.Monad            (forM_)
-import Data.Primitive.Array
 #endif
 
 import qualified Data.IntSet as IntSet
@@ -197,8 +198,8 @@ newClauseDB size = do
 
     return (CDB arr)
 
-insertClauseDB :: Clause2 -> ClauseDB s -> ST s ()
-insertClauseDB clause@(MkClause2 l1 l2 _) cdb = do
+insertClauseDB :: Lit -> Lit -> Clause2 -> ClauseDB s -> ST s ()
+insertClauseDB l1 l2 clause cdb = do
     insertWatch l1 (W l2 clause) cdb
     insertWatch l2 (W l1 clause) cdb
 
@@ -406,7 +407,9 @@ solve solver@Solver {..} = whenOk_ (simplify solver) $ do
 #ifdef TWO_WATCHED_LITERALS
     litCount <- readSTRef nextLit
     clauseDB <- newClauseDB litCount
-    forM_ clauses' $ \c -> insertClauseDB c clauseDB
+    forM_ clauses' $ \c -> satisfied2_ solution c >>= \case
+        Unresolved_ l1 l2 -> insertClauseDB l1 l2 c clauseDB
+        _                 -> error "PANIC! not simplified DB"
 #else
     let clauseDB = clauses'
 #endif