WIP

examples/sat-simple-sudoku.hs

@@ -76,8 +76,8 @@ initValues = 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 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)
@@ -89,8 +89,8 @@ initValues = N9
     (N9 5 3 0 0 7 0 0 0 0)
     (N9 6 0 0 1 9 5 0 0 0)
     (N9 0 9 8 0 0 0 0 6 0)
-    (N9 8 0 0 0 6 0 0 0 3)
 -}
+    (N9 8 0 0 0 6 0 0 0 3)
     (N9 4 0 0 8 0 3 0 0 1)
     (N9 7 0 0 0 2 0 0 0 6)
     (N9 0 6 0 0 0 0 2 8 0)

sat-simple-pure/DPLL.hs

@@ -432,8 +432,8 @@ forLitInClause2_ (MkClause2 l1 l2 ls) f =
 nullClause :: Clause2
 nullClause = MkClause2 (MkLit 1) (MkLit 1) emptyPrimArray
 
-nullClause3 :: Clause2
-nullClause3 = MkClause2 (MkLit 2) (MkLit 2) emptyPrimArray
+isNullClause :: Clause2 -> Bool
+isNullClause (MkClause2 l1 l2 _) = l1 == l2
 
 data Satisfied_
     = Satisfied_
@@ -604,6 +604,31 @@ unsat Solver {..} = do
     readSTRef variables >>= clearVarSet
     return False
 
+-------------------------------------------------------------------------------
+-- Trail
+-------------------------------------------------------------------------------
+
+data Trail
+    = End
+    | Deduced !Lit !Trail
+    | Decided !Lit !Trail
+  deriving Show
+
+traceTrail :: forall s. LitTable s Clause2 -> Trail -> ST s ()
+traceTrail reasons trail = do
+    ls <- go trail
+    traceM $ unlines $ "=== Trail ===" : ls
+  where
+    go :: Trail -> ST s [String]
+    go End = return ["=== ===== ==="]
+    go (Deduced l t) = do
+        c <- readLitTable reasons l
+        ls <- go t
+        return ((showString "Deduced " . showsPrec 11 l . showChar ' ' . showsPrec 11 c) "" : ls)
+    go (Decided l t) = do
+        ls <- go t
+        return ((showString "Decided " . showsPrec 11 l) "" : ls)
+
 -------------------------------------------------------------------------------
 -- Solving
 -------------------------------------------------------------------------------
@@ -631,36 +656,14 @@ data Self s = Self
       -- ^ sandbox used to construct conflict clause
     }
 
-data Trail
-    = End
-    | Deduced !Lit !Trail
-    | Decided !Lit !Trail
-  deriving Show
-
-traceTrail :: forall s. LitTable s Clause2 -> Trail -> ST s ()
-traceTrail reasons trail = do
-    ls <- go trail
-    traceM $ unlines ls
-  where
-    go :: Trail -> ST s [String]
-    go End = return ["End"]
-    go (Deduced l t) = do
-        c <- readLitTable reasons l
-        ls <- go t
-        return ((showString "Deduced " . showsPrec 11 l . showChar ' ' . showsPrec 11 c) "" : ls)
-    go (Decided l t) = do
-        ls <- go t
-        return ((showString "Decided " . showsPrec 11 l) "" : ls)
-
 solve :: Solver s -> ST s Bool
 solve solver@Solver {..} = whenOk_ (simplify solver) $ do
     clauses' <- readSTRef clauses
     vars     <- readSTRef variables
-    -- traceM $ "solve " ++ show (length clauses')
 
     litCount <- readSTRef nextLit
     units    <- newLitSet litCount
-    reasons  <- newLitTable litCount nullClause3
+    reasons  <- newLitTable litCount nullClause
     sandbox  <- newLitSet litCount
     pa       <- readSTRef solution