sat-simple (empty) → 0.1.0.0
raw patch · 7 files changed
+1377/−0 lines, 7 filesdep +basedep +containersdep +minisat
Dependencies added: base, containers, minisat, sat-simple, unliftio-core
Files
- CHANGELOG.md +3/−0
- LICENSE +30/−0
- examples/sat-simple-nonogram.hs +270/−0
- examples/sat-simple-sudoku.hs +225/−0
- examples/sat-simple-tseitin.hs +193/−0
- sat-simple.cabal +84/−0
- src/Control/Monad/SAT.hs +572/−0
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+# 0.1++Initial release
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2023, Oleg Grenrus++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Oleg Grenrus nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ examples/sat-simple-nonogram.hs view
@@ -0,0 +1,270 @@+module Main (main) where++import Control.Monad (forM, forM_)+import Control.Monad.IO.Class (liftIO)+import Data.Functor.Compose (Compose (..))+import Data.List (nub)+import Data.Map (Map)++import qualified Data.Map as Map++import Control.Monad.SAT++-------------------------------------------------------------------------------+-- Examples+-------------------------------------------------------------------------------++easyP :: ([[Int]], [[Int]])+easyP = ([[2], [1]], [[2],[1]])++-- | https://en.wikipedia.org/wiki/Nonogram#Example+problemP :: ([[Int]], [[Int]])+problemP = (rows, cols) where+ rows =+ [ []+ , [4]+ , [6]+ , [2,2]+ , [2,2]+ , [6]+ , [4]+ , [2]+ , [2]+ , [2]+ , []+ ]++ cols =+ [ []+ , [9]+ , [9]+ , [2,2]+ , [2,2]+ , [4]+ , [4]+ , []+ ]++-- | https://en.wikipedia.org/wiki/Nonogram#/media/File:Nonogram_wiki.svg+problemW :: ([[Int]], [[Int]])+problemW = (rows, cols) where+ rows =+ [ [8,7,5,7]+ , [5,4,3,3]+ , [3,3,2,3]+ , [4,3,2,2]+ , [3,3,2,2]+ , [3,4,2,2]+ , [4,5,2]+ , [3,5,1]+ , [4,3,2]+ , [3,4,2]+ , [4,4,2]+ , [3,6,2]+ , [3,2,3,1]+ , [4,3,4,2]+ , [3,2,3,2]+ , [6,5]+ , [4,5]+ , [3,3]+ , [3,3]+ , [1,1]+ ]++ cols =+ [ [1]+ , [1]+ , [2]+ , [4]+ , [7]+ , [9]+ , [2,8]+ , [1,8]+ , [8]+ , [1,9]+ , [2,7]+ , [3,4]+ , [6,4]+ , [8,5]+ , [1,11]+ , [1,7]+ , [8]+ , [1,4,8]+ , [6,8]+ , [4,7]+ , [2,4]+ , [1,4]+ , [5]+ , [1,4]+ , [1,5]+ , [7]+ , [5]+ , [3]+ , [1]+ , [1]+ ]+++-------------------------------------------------------------------------------+-- Main+-------------------------------------------------------------------------------++main :: IO ()+main = do+ nonogram "Easy" easyP+ nonogram "Letter P" problemP+ nonogram "Letter W" problemW+ where+ nonogram name p = do+ putStrLn name+ solP <- uncurry solveNonogram p+ putStrLn $ render solP++-------------------------------------------------------------------------------+-- Render+-------------------------------------------------------------------------------++render :: [[Bool]] -> String+render sol = unlines+ [ map (\b -> if b then '*' else ' ') l+ | l <- sol+ ]++-------------------------------------------------------------------------------+-- Solve+-------------------------------------------------------------------------------++solveNonogram :: [[Int]] -> [[Int]] -> IO [[Bool]]+solveNonogram rows cols = runSAT $ do+ let lits' :: [[SAT s (Lit s)]]+ lits' = [ [ newLit | _ <- cols ] | _ <- rows ]++ -- create solution variables.+ Compose lits <- sequence (Compose lits')++ -- row constraints+ forM_ (zip rows lits) $ \(r, ls) -> do+ regexp r ls++ -- column constraints+ forM_ (zip cols (transpose lits)) $ \(r, ls) -> do+ regexp r ls++ numberOfVariables >>= \n -> liftIO $ putStrLn $ "variables: " ++ show n+ numberOfClauses >>= \n -> liftIO $ putStrLn $ "clauses: " ++ show n++ -- solve+ Compose sol <- solve (Compose lits)++ return sol++transpose:: [[a]] -> [[a]]+transpose ([]:_) = []+transpose x = map head x : transpose (map tail x)++-------------------------------------------------------------------------------+-- NFA matching+-------------------------------------------------------------------------------++data RE a+ = Emp+ | Eps+ | Chr a+ | Rep (RE a)+ | App (RE a) (RE a)+ -- | Alt (RE a) (RE a)+ deriving (Eq, Ord, Show)++{-+alt :: RE a -> RE a -> RE a+alt Emp s = s+alt r Emp = r+alt (Alt r t) s = alt r (alt t s)+alt r s = Alt r s+-}++app :: RE a -> RE a -> RE a+app Emp _ = Emp+app _ Emp = Emp+app Eps s = s+app r Eps = r+app (App r t) s = app r (app t s)+app r s = App r s++nullable :: RE a -> Bool+nullable Emp = False+nullable Eps = True+nullable (Chr _) = False+nullable (Rep _) = True+nullable (App r1 r2) = nullable r1 && nullable r2+-- nullable (Alt r1 r2) = nullable r1 || nullable r2++derivate :: Eq a => a -> RE a -> [RE a]+derivate _ Emp = []+derivate _ Eps = []+derivate c (Chr c') = if c == c' then [Eps] else []+-- derivate c (Alt r s) = derivate c r ++ derivate c s+derivate c (Rep r) = [ app r' (Rep r) | r' <- derivate c r ]+derivate c (App r s)+ | nullable r = [ app r' s | r' <- derivate c r ] ++ derivate c s+ | otherwise = [ app r' s | r' <- derivate c r ]++derivateAny :: RE a -> [RE a]+derivateAny Emp = []+derivateAny Eps = []+derivateAny (Chr _) = [Eps]+derivateAny (Rep r) = [ app r' (Rep r) | r' <- derivateAny r ]+-- derivateAny (Alt r s) = derivateAny r ++ derivateAny s+derivateAny (App r s)+ | nullable r = [ app r' s | r' <- derivateAny r ] ++ derivateAny s+ | otherwise = [ app r' s | r' <- derivateAny r ]++-- | Does regexp accept any string of given length.+accepts :: Eq a => Int -> RE a -> Bool+accepts n r+ | n <= 0 = nullable r+ | otherwise = any (accepts (n - 1)) (nub (derivateAny r))++convert :: [Int] -> RE Bool+convert [] = Rep (Chr False)+convert (n:ns) = App (Rep (Chr False)) $ nOnes n $ convert ns+ where+ nOnes m r = if m >= 1 then App (Chr True) (nOnes (m - 1) r) else r++regexp :: forall s. [Int] -> [Lit s] -> SAT s ()+regexp r0 ls0 = do+ tl <- trueLit+ go [(tl, convert r0)] ls0+ where+ go :: [(Lit s, RE Bool)] -> [Lit s] -> SAT s ()+ go s [] = do+ -- we should have reached at least one nullable state+ assertAtLeastOne+ [ l+ | (l, r) <- s+ , nullable r+ ]++ go s (l:ls) = do+ -- next states with a list from which states they can be reached.+ let next :: Map (RE Bool) [(Lit s, Bool)]+ next = Map.fromListWith (++)+ [ (r', [(l', c)])+ | (l', r) <- s+ , c <- [True, False]+ -- nub doesn't seem to affect.+ , r' <- nub $ derivate c r+ , accepts (length ls) r'+ ]++ -- add definitions for the next NFA states,+ -- with their values depending on current `l` and previous states.+ s' <- forM (Map.toList next) $ \(r', steps) -> do+ n <- addDefinition $ foldr (\/) false+ [ lit l' /\ if b then lit l else neg (lit l)+ | (l', b) <- steps+ ]++ return (n, r')++ go s' ls
+ examples/sat-simple-sudoku.hs view
@@ -0,0 +1,225 @@+-- This example is the same as in @ersatz@+-- However+-- - we use different encoding.+-- - abuse Applicative/Traversable and symmetry of Sudoku+-- to avoid dealing with indices.+--+module Main (main) where++import Control.Applicative (liftA2)+import Control.Monad (when)+import Control.Monad.IO.Class (liftIO)+import Data.Foldable (for_, toList, traverse_)++import Control.Monad.SAT++-------------------------------------------------------------------------------+-- Main+-------------------------------------------------------------------------------++main :: IO ()+main = do+ putStrLn "Problem:"+ putStr $ render initValues+++ putStrLn "Solving..."+ sol <- runSAT $ do+ let stats = True++ m <- sudokuModel+ sudokuValues m initValues+ sudokuRules m++ when stats $ do+ numberOfVariables >>= \n -> liftIO $ putStrLn $ "variables: " ++ show n+ numberOfClauses >>= \n -> liftIO $ putStrLn $ "clauses: " ++ show n++ simplify++ when stats $ do+ numberOfClauses >>= \n -> liftIO $ putStrLn $ "clauses': " ++ show n++ sol <- solve m++ when stats $ do+ numberOfLearnts >>= \n -> liftIO $ putStrLn $ "learnts: " ++ show n+ numberOfConflicts >>= \n -> liftIO $ putStrLn $ "conflicts: " ++ show n+++ return sol++ putStrLn "Solution:"+ putStr $ render $ decode sol++-------------------------------------------------------------------------------+-- Initial values+-------------------------------------------------------------------------------++initValues :: Nine (Nine Int)+initValues = N9+ -- From https://en.wikipedia.org/w/index.php?title=Sudoku&oldid=543290082+ (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 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)+ (N9 0 0 0 4 1 9 0 0 5)+ (N9 0 0 0 0 8 0 0 7 9)++-------------------------------------------------------------------------------+-- Rendering+-------------------------------------------------------------------------------++render :: Nine (Nine Int) -> String+render sol = unlines $ renderGroups top divider bottom $ fmap renderLine sol+ where+ top = bar "┌" "───────" "┬" "┐"+ divider = bar "├" "───────" "┼" "┤"+ bottom = bar "└" "───────" "┴" "┘"++ bar begin fill middle end = begin ++ fill ++ middle ++ fill ++ middle ++ fill ++ end++renderLine :: Nine Int -> String+renderLine sol = unwords $ renderGroups "│" "│" "│" $ fmap showN sol+ where+ showN n | 1 <= n && n <= 9 = show n+ | otherwise = " "++renderGroups :: a -> a -> a -> Nine a -> [a]+renderGroups begin middle end (N (T xs ys zs)) =+ [begin] ++ toList xs ++ [middle] ++ toList ys ++ [middle] ++ toList zs ++ [end]++-------------------------------------------------------------------------------+-- Triple+-------------------------------------------------------------------------------++data Triple a = T a a a+ deriving (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)++instance Applicative Nine where+ pure x = N (pure (pure x))+ N f <*> N x = N (liftA2 (<*>) f x)++pattern N9 :: a -> a -> a -> a -> a -> a -> a -> a -> a -> Nine a+pattern N9 a b c d e f g h i = N (T (T a b c) (T d e f) (T g h i))+{-# COMPLETE N9 #-}++-------------------------------------------------------------------------------+-- Sudoku model+-------------------------------------------------------------------------------++-- | Model is nine rows of nine columns of nine bits.+newtype Model a = M (Nine (Nine (Nine a)))+ deriving (Functor, Foldable, Traversable)++emptyModel :: Model ()+emptyModel = M $ pure $ pure $ pure ()++decode :: Model Bool -> Nine (Nine Int)+decode (M m) = fmap (fmap f) m where+ f :: Nine Bool -> Int+ f (N9 X _ _ _ _ _ _ _ _) = 1+ f (N9 _ X _ _ _ _ _ _ _) = 2+ f (N9 _ _ X _ _ _ _ _ _) = 3+ f (N9 _ _ _ X _ _ _ _ _) = 4+ f (N9 _ _ _ _ X _ _ _ _) = 5+ f (N9 _ _ _ _ _ X _ _ _) = 6+ f (N9 _ _ _ _ _ _ X _ _) = 7+ f (N9 _ _ _ _ _ _ _ X _) = 8+ f (N9 _ _ _ _ _ _ _ _ X) = 9+ f _ = 0++pattern X :: Bool+pattern X = True++-------------------------------------------------------------------------------+-- SAT rules+-------------------------------------------------------------------------------++-- | Populate model with the literals.+sudokuModel :: SAT s (Model (Lit s))+sudokuModel = traverse (\_ -> newLit) emptyModel++-- | Sudoku rules.+--+-- Add constraints of the puzzle.+sudokuRules :: Model (Lit s) -> SAT s ()+sudokuRules model = do+ -- each "digit" is 1..9+ -- we encode digits using 9 bits.+ -- exactly one, i.e. at most one and and least one have to set.+ forDigit_ model $ \d -> do+ let lits = toList d+ assertAtMostOne lits+ assertAtLeastOne lits++ -- With above digit encoding the sudoku rules are easy to encode:+ -- For each row we should have at least one 1, at least one 2, ... 9+ -- And similarly for columns and subsquares.+ --+ -- If we also require that each row, column and subsquare has at most one 1..9+ -- the given problem becomes trivial, as is solved by initial unit propagation.++ -- each row+ forRow_ model $ \block -> do+ let block' = sequenceA block+ for_ block' $ \d -> do+ let lits = toList d+ assertAtLeastOne lits+ -- assertAtMostOne lits++ -- each column+ forColumn_ model $ \block -> do+ let block' = sequenceA block+ for_ block' $ \d -> do+ let lits = toList d+ assertAtLeastOne lits+ -- assertAtMostOne lits++ -- each subsquare+ forSubSq_ model $ \block -> do+ let block' = sequenceA block+ for_ block' $ \d -> do+ let lits = toList d+ assertAtLeastOne lits+ -- assertAtMostOne lits++forDigit_ :: Applicative f => Model a -> (Nine a -> f b) -> f ()+forDigit_ (M m) f = traverse_ (traverse_ f) m++forRow_ :: Applicative f => Model a -> (Nine (Nine a) -> f b) -> f ()+forRow_ (M m) f = traverse_ f m++forColumn_ :: Applicative f => Model a -> (Nine (Nine a) -> f b) -> f ()+forColumn_ (M m) f = traverse_ f (sequenceA m)++forSubSq_ :: Applicative f => Model a -> (Nine (Nine a) -> f b) -> f ()+forSubSq_ (M m) f = traverse_ f $ fmap N $ N $ fmap sequenceA $ unN $ fmap unN m++-- | Add constraints of the initial setup.+sudokuValues :: Model (Lit s) -> Nine (Nine Int) -> SAT s ()+sudokuValues (M m) v = traverse_ sequenceA $ liftA2 (liftA2 f) m v+ where+ -- force the corresponding bit.+ f :: Nine (Lit s) -> Int -> SAT s ()+ f (N9 l _ _ _ _ _ _ _ _) 1 = addClause [l]+ f (N9 _ l _ _ _ _ _ _ _) 2 = addClause [l]+ f (N9 _ _ l _ _ _ _ _ _) 3 = addClause [l]+ f (N9 _ _ _ l _ _ _ _ _) 4 = addClause [l]+ f (N9 _ _ _ _ l _ _ _ _) 5 = addClause [l]+ f (N9 _ _ _ _ _ l _ _ _) 6 = addClause [l]+ f (N9 _ _ _ _ _ _ l _ _) 7 = addClause [l]+ f (N9 _ _ _ _ _ _ _ l _) 8 = addClause [l]+ f (N9 _ _ _ _ _ _ _ _ l) 9 = addClause [l]++ f _ _ = return ()
+ examples/sat-simple-tseitin.hs view
@@ -0,0 +1,193 @@+module Main (main) where++import Control.Applicative (liftA2)+import Control.Monad (void)+import Control.Monad.IO.Class (liftIO)+import Data.Foldable (toList)++import Control.Monad.SAT++data H3 a = H3 a a a+ deriving (Show, Functor, Foldable, Traversable)++instance Applicative H3 where+ pure x = H3 x x x+ H3 f1 f2 f3 <*> H3 x1 x2 x3 = H3 (f1 x1) (f2 x2) (f3 x3)++data H5 a = H5 a a a a a+ deriving (Show, Functor, Foldable, Traversable)++instance Applicative H5 where+ pure x = H5 x x x x x+ H5 f1 f2 f3 f4 f5 <*> H5 x1 x2 x3 x4 x5 = H5 (f1 x1) (f2 x2) (f3 x3) (f4 x4) (f5 x5)++eval :: H5 Bool -> Bool+eval (H5 p q r s t) =+ not ((p && q) == r) && (impl s (p && t))+ where+ impl x y = not x || y++title :: String -> IO ()+title s = do+ putStrLn ""+ putStrLn s+ putStrLn $ '-' <$ s++main :: IO ()+main = do+ title "addDefinition >>= addClause . singleton"+ void $ runSATMaybe $ do+ -- ~ ((p /\ q) <-> r) /\ (s -> (p /\ t))+ p <- newLit+ q <- newLit+ r <- newLit+ s <- newLit+ t <- newLit+ let prop = neg ((lit p /\ lit q) <-> lit r) /\ (lit s --> (lit p /\ lit t))+ liftIO $ print prop+ f <- addDefinition prop+ addClause [f]++ let lits = H5 p q r s t++ let loop = do+ res <- solve lits+ liftIO $ print (eval res, res)++ let n True l = neg l+ n False l = l++ addClause $ toList $ liftA2 n res lits++ loop++ loop++ title "addProp"+ void $ runSATMaybe $ do+ -- ~ ((p /\ q) <-> r) /\ (s -> (p /\ t))+ p <- newLit+ q <- newLit+ r <- newLit+ s <- newLit+ t <- newLit++ addProp $ neg ((lit p /\ lit q) <-> lit r) /\ (lit s --> (lit p /\ lit t))+ let lits = H5 p q r s t++ let loop = do+ res <- solve lits+ liftIO $ print (eval res, res)++ let n True l = neg l+ n False l = l++ addClause $ toList $ liftA2 n res lits++ loop++ loop++ title "Same using addProp"+ void $ runSATMaybe $ do+ p <- newLit+ q <- newLit+ r <- newLit+ s <- newLit+ t <- newLit++ let prop = (lit p /\ lit q /\ lit r /\ lit s /\ lit t) \/ (neg (lit p) /\ neg (lit q) /\ neg (lit r) /\ neg (lit s) /\ neg (lit t))+ liftIO $ print prop+ addProp prop+ let lits = H5 p q r s t++ let loop = do+ res <- solve lits+ liftIO $ print res++ let n True l = neg l+ n False l = l++ addClause $ toList $ liftA2 n res lits++ loop++ loop++ title "Same using assertAllEqual"+ void $ runSATMaybe $ do+ p <- newLit+ q <- newLit+ r <- newLit+ s <- newLit+ t <- newLit++ assertAllEqual [p, q, r, s, t]+ let lits = H5 p q r s t++ let loop = do+ res <- solve lits+ liftIO $ print res++ let n True l = neg l+ n False l = l++ addClause $ toList $ liftA2 n res lits++ loop++ loop++ title "Same using <->"+ void $ runSATMaybe $ do+ p <- newLit+ q <- newLit+ r <- newLit+ s <- newLit+ t <- newLit++ let prop = (lit p <-> lit q) /\+ (lit q <-> lit r) /\+ (lit r <-> lit s) /\+ (lit s <-> lit t)+ liftIO $ print prop+ addProp prop+ let lits = H5 p q r s t++ let loop = do+ res <- solve lits+ liftIO $ print res++ let n True l = neg l+ n False l = l++ addClause $ toList $ liftA2 n res lits++ loop++ loop++ title "if-then-else"+ void $ runSATMaybe $ do+ c <- newLit+ t <- newLit+ f <- newLit++ let prop = ite (lit c) (lit t) (lit f)+ liftIO $ putStrLn $ "prop = " ++ show prop+ -- addProp prop+ addDefinition prop >>= addClause . pure++ let lits = H3 c t f+ let loop = do+ res <- solve lits+ liftIO $ print res++ let n True l = neg l+ n False l = l++ addClause $ toList $ liftA2 n res lits++ loop++ loop
+ sat-simple.cabal view
@@ -0,0 +1,84 @@+cabal-version: 2.4+name: sat-simple+version: 0.1.0.0+synopsis: A high-level wrapper over minisat+description:+ A high-level wrapper over minisat.+ .+ This package differs from [@ersatz@](https://hackage.haskell.org/package/ersatz) in few ways:+ .+ * The interface resembles 'ST' monad, with 'SAT' monad and literals 'Lit' are indexed by a scope @s@ type argument.+ .+ * @sat-simple@ uses @minisat@'s library in incremental way, instead of encoding to DIMACS format and spawning processes.+ (@ersatz@ can be made to use @minisat@ library as well, but it cannot use incrementality AFAICT).+ .+ * @sat-simple@ has less encodings built-in+ .+ * @sat-simple@ is hopefully is indeed simpler to use.++license: BSD-3-Clause+license-file: LICENSE+author: Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+copyright: 2023 Oleg Grenrus+category: Data+build-type: Simple+extra-doc-files: CHANGELOG.md+tested-with:+ GHC ==8.6.5+ || ==8.8.5+ || ==8.10.7+ || ==9.0.2+ || ==9.2.8+ || ==9.4.7+ || ==9.6.3+ || ==9.8.1++common language+ default-language: Haskell2010+ default-extensions:+ DeriveTraversable+ GADTs+ PatternSynonyms+ PatternSynonyms+ RankNTypes+ RoleAnnotations+ ScopedTypeVariables++library+ import: language+ hs-source-dirs: src+ exposed-modules: Control.Monad.SAT+ build-depends:+ , base >=4.12 && <4.20+ , containers ^>=0.6.0.1+ , minisat ^>=0.1.3+ , unliftio-core ^>=0.2.1.0++test-suite sat-simple-sudoku+ import: language+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: sat-simple-sudoku.hs+ build-depends:+ , base+ , sat-simple++test-suite sat-simple-nonogram+ import: language+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: sat-simple-nonogram.hs+ build-depends:+ , base+ , containers+ , sat-simple++test-suite sat-simple-tseitin+ import: language+ type: exitcode-stdio-1.0+ hs-source-dirs: examples+ main-is: sat-simple-tseitin.hs+ build-depends:+ , base+ , sat-simple
+ src/Control/Monad/SAT.hs view
@@ -0,0 +1,572 @@+-- | A monadic interface to the SAT (@minisat@) solver.+--+-- The interface is inspired by ST monad. 'SAT' and 'Lit' are indexed by a "state" token,+-- so you cannot mixup literals from different SAT computations.+module Control.Monad.SAT (+ -- * SAT Monad+ SAT,+ runSAT,+ runSATMaybe,+ UnsatException (..),+ -- * Literals+ Lit,+ newLit,+ -- ** Negation+ Neg (..),+ -- * Clauses+ addClause,+ assertAtLeastOne,+ assertAtMostOne,+ assertAtMostOnePairwise,+ assertAtMostOneSequential,+ assertEqual,+ assertAllEqual,+ -- ** Propositional formulas+ Prop,+ true, false,+ lit, (\/), (/\), (<->), (-->), xor, ite,+ addDefinition,+ addProp,+ -- ** Clause definitions+ trueLit,+ falseLit,+ addConjDefinition,+ addDisjDefinition,+ -- * Solving+ solve,+ solve_,+ -- * Simplification+ simplify,+ -- * Statistics+ numberOfVariables,+ numberOfClauses,+ numberOfLearnts,+ numberOfConflicts,+) where++import Control.Exception (Exception, catch, throwIO)+import Control.Monad (forM_, unless)+import Control.Monad.IO.Class (MonadIO (..))+import Control.Monad.IO.Unlift (MonadUnliftIO (..))+import Data.Bits (shiftR, testBit)+import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import Data.List (tails)+import Data.Map.Strict (Map)+import Data.Set (Set)+import GHC.Exts (oneShot)++import qualified Data.Map.Strict as Map+import qualified Data.Set as Set+import qualified MiniSat++-------------------------------------------------------------------------------+-- SAT Monad+-------------------------------------------------------------------------------++-- | Satisfiability monad.+newtype SAT s a = SAT_ { unSAT :: MiniSat.Solver -> Lit s -> IORef (Definitions s) -> IO a }+ deriving Functor++-- The SAT monad environment consists of+-- * A solver instance+-- * A literal constraint to be true.+-- * A map of asserted definitions, to dedup these for 'addDefinitions' and 'addProp' calls.+-- (we don't dedup clauses though - it's up to the solver).++type role SAT nominal representational++pattern SAT :: forall s a. (MiniSat.Solver -> Lit s -> IORef (Definitions s) -> IO a) -> SAT s a+pattern SAT m <- SAT_ m+ where SAT m = SAT_ (oneShot m)+{-# COMPLETE SAT #-}++type Definitions s = Map (Set (Lit s)) (Lit s)++-- | Unsatisfiable exception.+--+-- It may be thrown by various functions: in particular 'solve' and 'solve_', but also 'addClause', 'simplify'.+--+-- The reason to use an exception is because after unsatisfiable state is reached the underlying solver instance is unusable.+-- You may use 'runSATMaybe' to catch it.+data UnsatException = UnsatException+ deriving (Show)++instance Exception UnsatException++data SATPanic = SATPanic+ deriving (Show)++instance Exception SATPanic++instance Applicative (SAT s) where+ pure x = SAT (\_ _ _ -> pure x)+ SAT f <*> SAT x = SAT (\s t r -> f s t r <*> x s t r)++instance Monad (SAT s) where+ m >>= k = SAT $ \s t r -> do+ x <- unSAT m s t r+ unSAT (k x) s t r++instance MonadIO (SAT s) where+ liftIO m = SAT (\_ _ _ -> m)++instance MonadUnliftIO (SAT s) where+ withRunInIO kont = SAT $ \s t r -> kont (\(SAT m) -> m s t r)++-- | Run 'SAT' computation.+runSAT :: (forall s. SAT s a) -> IO a+runSAT (SAT f) = MiniSat.withNewSolverAsync $ \s -> do+ t <- MiniSat.newLit s+ add_clause s [L t]+ r <- newIORef Map.empty+ f s (L t) r++-- | Run 'SAT' computation. Return 'Nothing' if 'UnsatException' is thrown.+runSATMaybe :: (forall s. SAT s a) -> IO (Maybe a)+runSATMaybe m = fmap Just (runSAT m) `catch` \UnsatException -> return Nothing++-------------------------------------------------------------------------------+-- Literals+-------------------------------------------------------------------------------++-- | Literal.+--+-- To negate literate use 'neg'.+newtype Lit s = L { unL :: MiniSat.Lit }+ deriving (Eq, Ord)++type role Lit nominal++instance Show (Lit s) where+ showsPrec d (L (MiniSat.MkLit l))+ | p = showParen (d > 6) (showChar '-' . shows v)+ | otherwise = shows v+ where+ i :: Int+ i = fromIntegral l++ -- minisat encodes polarity of literal in 0th bit.+ -- (this way normal order groups same variable literals).+ p :: Bool+ p = testBit i 0++ v :: Int+ v = shiftR i 1++class Neg a where+ neg :: a -> a++-- | Negate literal.+instance Neg (Lit s) where+ neg (L l) = L (MiniSat.neg l)++-- | Create fresh literal.+newLit :: SAT s (Lit s)+newLit = SAT $ \s _t _r -> do+ l <- MiniSat.newLit s+ return (L l)++-------------------------------------------------------------------------------+-- Prop+-------------------------------------------------------------------------------++-- | Propositional formula.+data Prop s+ = PTrue+ | PFalse+ | P (Prop1 s)+ deriving (Eq, Ord)++infixr 5 \/+infixr 6 /\++instance Show (Prop s) where+ showsPrec _ PTrue = showString "true"+ showsPrec _ PFalse = showString "false"+ showsPrec d (P p) = showsPrec d p++-- | True 'Prop'.+true :: Prop s+true = PTrue++-- | False 'Prop'.+false :: Prop s+false = PFalse++-- | Make 'Prop' from a literal.+lit :: Lit s -> Prop s+lit l = P (P1Lit l)++-- | Disjunction of propositional formulas, or.+(\/) :: Prop s -> Prop s -> Prop s+x \/ y = neg (neg x /\ neg y)++-- | Conjunction of propositional formulas, and.+(/\) :: Prop s -> Prop s -> Prop s+PFalse /\ _ = PFalse+_ /\ PFalse = PFalse+PTrue /\ y = y+x /\ PTrue = x+P x /\ P y = P (p1and x y)++-- | Implication of propositional formulas.+(-->) :: Prop s -> Prop s -> Prop s+x --> y = neg x \/ y++-- | Equivalence of propositional formulas.+(<->) :: Prop s -> Prop s -> Prop s+x <-> y = (x --> y) /\ (y --> x)++-- | Exclusive or, not equal of propositional formulas.+xor :: Prop s -> Prop s -> Prop s+xor x y = x <-> neg y++-- | If-then-else.+--+-- Semantics of @'ite' c t f@ are @ (c '/\' t) '\/' ('neg' c '/\' f)@.+--+ite :: Prop s -> Prop s -> Prop s -> Prop s+-- ite c t f = (c /\ t) \/ (neg c /\ f)+ite c t f = (c \/ f) /\ (neg c \/ t) /\ (t \/ f) -- this encoding makes (t == f) case propagate even when c is yet undecided.++-- | Negation of propositional formulas.+instance Neg (Prop s) where+ neg PTrue = PFalse+ neg PFalse = PTrue+ neg (P p) = P (p1neg p)++-------------------------------------------------------------------------------+-- Prop1+-------------------------------------------------------------------------------++data Prop1 s+ = P1Lit !(Lit s)+ | P1Nnd !(Set (PropA s))+ | P1And !(Set (PropA s))+ deriving (Eq, Ord)++data PropA s+ = PALit !(Lit s)+ | PANnd !(Set (PropA s))+ deriving (Eq, Ord)++instance Show (Prop1 s) where+ showsPrec d (P1Lit l) = showsPrec d l+ showsPrec _ (P1And xs) = showNoCommaListWith shows (Set.toList xs)+ showsPrec _ (P1Nnd xs) = showChar '-' . showNoCommaListWith shows (Set.toList xs)++instance Show (PropA s) where+ showsPrec d (PALit l) = showsPrec d l+ showsPrec _ (PANnd xs) = showChar '-' . showNoCommaListWith shows (Set.toList xs)++showNoCommaListWith :: (a -> ShowS) -> [a] -> ShowS+showNoCommaListWith _ [] s = "[]" ++ s+showNoCommaListWith showx (x:xs) s = '[' : showx x (showl xs)+ where+ showl [] = ']' : s+ showl (y:ys) = ' ' : showx y (showl ys)++p1and :: Prop1 s -> Prop1 s -> Prop1 s+p1and p@(P1Lit x) (P1Lit y)+ | x == y = p+ | otherwise = P1And (double (PALit x) (PALit y))+p1and p@(P1Nnd x) (P1Nnd y)+ | x == y = p+ | otherwise = P1And (double (PANnd x) (PANnd y))+p1and (P1Lit x) (P1Nnd y) = P1And (double (PALit x) (PANnd y))+p1and (P1Nnd x) (P1Lit y) = P1And (double (PANnd x) (PALit y))+p1and (P1Lit x) (P1And ys) = P1And (Set.insert (PALit x) ys)+p1and (P1Nnd x) (P1And ys) = P1And (Set.insert (PANnd x) ys)+p1and (P1And xs) (P1Lit y) = P1And (Set.insert (PALit y) xs)+p1and (P1And xs) (P1Nnd y) = P1And (Set.insert (PANnd y) xs)+p1and (P1And xs) (P1And ys) = P1And (Set.union xs ys)++p1neg :: Prop1 s -> Prop1 s+p1neg (P1Lit l) = P1Lit (neg l)+p1neg (P1Nnd xs) = P1And xs+p1neg (P1And xs) = P1Nnd xs++double :: Ord a => a -> a -> Set a+double x y = Set.insert x (Set.singleton y)++-------------------------------------------------------------------------------+-- Clause definitions+-------------------------------------------------------------------------------++-- | Add conjunction definition.+--+-- @addConjDefinition x ys@ asserts that @x ↔ ⋀ yᵢ@+addConjDefinition :: Lit s -> [Lit s] -> SAT s ()+addConjDefinition x zs = do+ y <- add_definition (Set.fromList zs)+ if x == y+ then return ()+ else assertEqual x y++-- | Add disjunction definition.+--+-- @addDisjDefinition x ys@ asserts that @x ↔ ⋁ yᵢ@+--+addDisjDefinition :: Lit s -> [Lit s] -> SAT s ()+addDisjDefinition x ys = addConjDefinition (neg x) (fmap neg ys)+-- Implementation: @(x ↔ ⋁ yᵢ) ↔ (¬x ↔ ⋀ ¬xyᵢ)@++-------------------------------------------------------------------------------+-- Methods+-------------------------------------------------------------------------------++-- | Assert that given 'Prop' is true.+--+-- This is equivalent to+--+-- @+-- addProp p = do+-- l <- addDefinition p+-- addClause l+-- @+--+-- but avoid creating the definition, asserting less clauses.+--+addProp :: Prop s -> SAT s ()+addProp PTrue = return ()+addProp PFalse = SAT $ \s t _ -> add_clause s [neg t]+addProp (P p) = add_prop p++-- | Add definition of 'Prop'. The resulting literal is equivalent to the argument 'Prop'.+--+addDefinition :: Prop s -> SAT s (Lit s)+addDefinition PTrue = trueLit+addDefinition PFalse = falseLit+addDefinition (P p) = addDefinition1 p++-- | True literal.+trueLit :: SAT s (Lit s)+trueLit = SAT $ \_s t _ -> return t++-- | False literal+falseLit :: SAT s (Lit s)+falseLit = SAT $ \_s t _ -> return (neg t)++addDefinition1 :: Prop1 s -> SAT s (Lit s)+addDefinition1 = tseitin1++-- | Add conjuctive definition.+add_definition :: Set (Lit s) -> SAT s (Lit s)+add_definition ps+ | Set.null ps+ = trueLit++add_definition ps = SAT $ \s _ defsRef -> do+ defs <- readIORef defsRef+ case Map.lookup ps defs of+ Just d -> return d+ Nothing -> do+ d' <- MiniSat.newLit s+ let d = L d'++ -- putStrLn $ "add_definition " ++ show (Set.toList ps) ++ " = " ++ show d++ -- d ∨ ¬x₁ ∨ ¬x₂ ∨ ... ∨ ¬xₙ+ add_clause s $ d : map neg (Set.toList ps)++ -- ¬d ∨ x₁+ -- ¬d ∨ x₂+ -- ...+ -- ¬d ∨ xₙ+ forM_ ps $ \p -> do+ add_clause s [neg d, p]++ -- save the definition.+ writeIORef defsRef $! Map.insert ps d defs++ return d++-- top-level add prop: CNF+add_prop :: Prop1 s -> SAT s ()+add_prop (P1Lit l) = addClause [l]+add_prop (P1And xs) = forM_ xs add_prop'+add_prop (P1Nnd xs) = do+ ls <- traverse tseitinA (Set.toList xs)+ addClause (map neg ls)++-- first-level: Clauses+add_prop' :: PropA s -> SAT s ()+add_prop' (PALit l) = addClause [l]+add_prop' (PANnd xs) = do+ ls <- traverse tseitinA (Set.toList xs)+ addClause (map neg ls)++tseitin1 :: Prop1 s -> SAT s (Lit s)+tseitin1 (P1Lit l) = return l+tseitin1 (P1And xs) = do+ xs' <- traverse tseitinA (Set.toList xs)+ add_definition (Set.fromList xs')+tseitin1 (P1Nnd xs) = do+ xs' <- traverse tseitinA (Set.toList xs)+ neg <$> add_definition (Set.fromList xs')++tseitinA :: PropA s -> SAT s (Lit s)+tseitinA (PALit l) = return l+tseitinA (PANnd xs) = do+ xs' <- traverse tseitinA (Set.toList xs)+ neg <$> add_definition (Set.fromList xs')++-------------------------------------------------------------------------------+-- Constraints+-------------------------------------------------------------------------------++-- | Add a clause to the solver.+addClause :: [Lit s] -> SAT s ()+addClause ls = SAT $ \s _t _r -> add_clause s ls++add_clause :: MiniSat.Solver -> [Lit s] -> IO ()+add_clause s ls = do+ -- putStrLn $ "add_clause " ++ show ls+ ok <- MiniSat.addClause s (map unL ls)+ unless ok $ throwIO UnsatException++-- | At least one -constraint.+--+-- Alias to 'addClause'.+assertAtLeastOne :: [Lit s] -> SAT s ()+assertAtLeastOne = addClause++-- | At most one -constraint.+--+-- Uses 'atMostOnePairwise' for lists of length 2 to 5+-- and 'atMostOneSequential' for longer lists.+--+-- The cutoff is chosen by picking encoding with least clauses:+-- For 5 literals, 'atMostOnePairwise' needs 10 clauses and 'assertAtMostOneSequential' needs 11 (and 4 new variables).+-- For 6 literals, 'atMostOnePairwise' needs 15 clauses and 'assertAtMostOneSequential' needs 14.+--+assertAtMostOne :: [Lit s] -> SAT s ()+assertAtMostOne ls = case ls of+ [] -> return ()+ [_] -> return ()+ [_,_] -> assertAtMostOnePairwise ls+ [_,_,_] -> assertAtMostOnePairwise ls+ [_,_,_,_] -> assertAtMostOnePairwise ls+ [_,_,_,_,_] -> assertAtMostOnePairwise ls+ _ -> assertAtMostOneSequential ls++-- | At most one -constraint using pairwise encoding.+--+-- \[+-- \mathrm{AMO}(x_1, \ldots, x_n) = \bigwedge_{1 \le i < j \le n} \neg x_i \lor \neg x_j+-- \]+--+-- \(n(n-1)/2\) clauses, zero auxiliary variables.+--+assertAtMostOnePairwise :: [Lit s] -> SAT s ()+assertAtMostOnePairwise literals = mapM_ f (tails literals) where+ f :: [Lit s] -> SAT s ()+ f [] = return ()+ f (l:ls) = mapM_ (g l) ls++ g :: Lit s -> Lit s -> SAT s ()+ g l1 l2 = addClause [neg l1, neg l2]++-- | At most one -constraint using sequential counter encoding.+--+-- \[+-- \mathrm{AMO}(x_1, \ldots, x_n) =+-- (\neg x_1 \lor s_1) \land+-- (\neg x_n \lor \neg s_{n-1}) \land+-- \bigwedge_{1 < i < n} (\neg x_i \lor a_i) \land (\neg a_{i-1} \lor a_i) \land (\neg x_i \lor \neg a_{i-1})+-- \]+--+-- Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality constraints, Proceedings of Principles and Practice of Constraint Programming (CP), 827–831 (2005)+--+-- \(3n-4\) clauses, \(n-1\) auxiliary variables.+--+-- We optimize the two literal case immediately ([resolution](https://en.wikipedia.org/wiki/Resolution_(logic)) on \(s_1\).+--+-- \[+-- (\neg x_1 \lor s_1) \land (\neg x_2 \lor \neg s_1) \Longrightarrow \neg x_1 \lor \neg x_2+-- \]+--+assertAtMostOneSequential :: [Lit s] -> SAT s ()+assertAtMostOneSequential [] = return ()+assertAtMostOneSequential [_] = return ()+assertAtMostOneSequential [x1,x2] = addClause [neg x1, neg x2]+assertAtMostOneSequential (xn:x1:xs) = do+ a1 <- newLit+ addClause [neg x1, a1]+ go a1 xs+ where+ go an1 [] = addClause [neg xn, neg an1]+ go ai1 (xi:xis) = do+ ai <- newLit+ addClause [neg xi, ai]+ addClause [neg ai1, ai]+ addClause [neg xi, neg ai1]+ go ai xis++-- | Assert that two literals are equal.+assertEqual :: Lit s -> Lit s -> SAT s ()+assertEqual l l'+ | l == l' = return ()+ | otherwise = do+ addClause [l, neg l']+ addClause [neg l, l']++-- | Assert that all literals in the list are equal.+assertAllEqual :: [Lit s] -> SAT s ()+assertAllEqual [] = return ()+assertAllEqual (l:ls) = forM_ (Set.fromList ls) $ \l' -> assertEqual l l'++-------------------------------------------------------------------------------+-- Solving+-------------------------------------------------------------------------------++-- | Search without returning a model.+solve_ :: SAT s ()+solve_ = SAT $ \s _t _r -> do+ ok <- MiniSat.solve s []+ unless ok $ throwIO UnsatException++-- | Search and return a model.+solve :: Traversable model => model (Lit s) -> SAT s (model Bool)+solve model = SAT $ \s _t _r -> do+ ok <- MiniSat.solve s []+ unless ok $ throwIO UnsatException++ traverse (getSym s) model+ where+ getSym :: MiniSat.Solver -> Lit s -> IO Bool+ getSym s (L l) = do+ b <- MiniSat.modelValue s l+ case b of+ Nothing -> throwIO SATPanic+ Just b' -> return b'++-------------------------------------------------------------------------------+-- Simplification+-------------------------------------------------------------------------------++-- | Removes already satisfied clauses.+simplify :: SAT s ()+simplify = SAT $ \s _t _r -> do+ ok <- MiniSat.simplify s+ unless ok $ throwIO UnsatException++-------------------------------------------------------------------------------+-- Statistics+-------------------------------------------------------------------------------++-- | The current number of variables.+numberOfVariables :: SAT s Int+numberOfVariables = SAT $ \s _t _r -> MiniSat.minisat_num_vars s++-- | The current number of original clauses.+numberOfClauses :: SAT s Int+numberOfClauses = SAT $ \s _t _r -> MiniSat.minisat_num_clauses s++-- | The current number of learnt clauses.+numberOfLearnts :: SAT s Int+numberOfLearnts = SAT $ \s _t _r -> MiniSat.minisat_num_learnts s++-- | The current number of conflicts.+numberOfConflicts :: SAT s Int+numberOfConflicts = SAT $ \s _t _r -> MiniSat.minisat_num_conflicts s