diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1 + +Initial release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/examples/sat-simple-nonogram.hs b/examples/sat-simple-nonogram.hs new file mode 100644 --- /dev/null +++ b/examples/sat-simple-nonogram.hs @@ -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 diff --git a/examples/sat-simple-sudoku.hs b/examples/sat-simple-sudoku.hs new file mode 100644 --- /dev/null +++ b/examples/sat-simple-sudoku.hs @@ -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 () diff --git a/examples/sat-simple-tseitin.hs b/examples/sat-simple-tseitin.hs new file mode 100644 --- /dev/null +++ b/examples/sat-simple-tseitin.hs @@ -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 diff --git a/sat-simple.cabal b/sat-simple.cabal new file mode 100644 --- /dev/null +++ b/sat-simple.cabal @@ -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 +maintainer: Oleg Grenrus +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 diff --git a/src/Control/Monad/SAT.hs b/src/Control/Monad/SAT.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/SAT.hs @@ -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