diff --git a/.hlint.yaml b/.hlint.yaml --- a/.hlint.yaml +++ b/.hlint.yaml @@ -6,6 +6,11 @@ - ignore: name: Use lambda-case +- ignore: + name: Use || # We define a different `or` + +- ignore: + name: Use && # We define a different `and` + - ignore: {name: Hoist not, within: [Ersatz.Bit]} # This is how we define `any`, ya dingus -- ignore: {name: Use ||, within: [Ersatz.Relation.Prop]} # This is a different `or` -- ignore: {name: Use &&, within: [Ersatz.Relation.Prop]} # This is a different `and` +- ignore: {name: Use infix, within: [Ersatz.Relation.Op]} # We define a different `union` function in this module diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,17 @@ +0.6 [2025.06.17] +---------------- +* Add the `Ersatz.Relation.ARS` module +* Change the type of `buildFrom`: + + ```diff + -buildFrom :: (Ix a, Ix b) => (a -> b -> Bit) -> ((a,b),(a,b)) -> Relation a b + +buildFrom :: (Ix a, Ix b) => ((a,b),(a,b)) -> ((a,b) -> Bit) -> Relation a b + ``` +* Add support for `kissat` and the `lingeling` trio (`lingeling`, `plingeling`, + `treengeling`) of SAT solvers. +* Add QBF examples (requires DepQBF solver) +* Replace `test-framework` with `tasty` in the test suite. + 0.5 [2023.09.08] ---------------- * The `forall` function in `Ersatz.Variable` has been renamed to diff --git a/ersatz.cabal b/ersatz.cabal --- a/ersatz.cabal +++ b/ersatz.cabal @@ -1,5 +1,5 @@ name: ersatz -version: 0.5 +version: 0.6 license: BSD3 license-file: LICENSE author: Edward A. Kmett, Eric Mertens, Johan Kiviniemi @@ -82,9 +82,12 @@ , GHC == 8.8.4 , GHC == 8.10.7 , GHC == 9.0.2 - , GHC == 9.2.7 - , GHC == 9.4.5 - , GHC == 9.6.2 + , GHC == 9.2.8 + , GHC == 9.4.8 + , GHC == 9.6.6 + , GHC == 9.8.4 + , GHC == 9.10.1 + , GHC == 9.12.1 extra-source-files: .gitignore .hlint.yaml @@ -155,7 +158,7 @@ source-repository head type: git - location: git://github.com/ekmett/ersatz.git + location: https://github.com/ekmett/ersatz.git flag examples description: Build examples @@ -171,8 +174,8 @@ array >= 0.2 && < 0.6, base >= 4.9 && < 5, bytestring >= 0.10.4.0 && < 0.13, - containers >= 0.2.0.1 && < 0.7, - data-default >= 0.5 && < 0.8, + containers >= 0.2.0.1 && < 0.9, + data-default >= 0.5 && < 0.9, lens >= 4 && < 6, mtl >= 1.1 && < 2.4, process >= 1.1 && < 1.7, @@ -197,6 +200,8 @@ Ersatz.Solution Ersatz.Solver Ersatz.Solver.DepQBF + Ersatz.Solver.Kissat + Ersatz.Solver.Lingeling Ersatz.Solver.Minisat Ersatz.Solver.Z3 Ersatz.Variable @@ -210,6 +215,7 @@ Ersatz.Relation.Data Ersatz.Relation.Prop Ersatz.Relation.Op + Ersatz.Relation.ARS executable ersatz-regexp-grid -- description: An example program that solves the regular expression crossword problem using Ersatz. @@ -252,6 +258,39 @@ ghc-options: -Wall hs-source-dirs: examples/sudoku +executable ersatz-graph-coloring + -- description: An example program that solves a graph coloring problem using Ersatz. + if flag(examples) + build-depends: + array, + base < 5, + bytestring, + ersatz, + mtl, + optparse-applicative + else + buildable: False + default-language: Haskell2010 + main-is: Coloring.hs + ghc-options: -Wall + hs-source-dirs: examples/qbf + +executable ersatz-circuit-synthesis + -- description: An example program that solves a circuit synthesis problem using Ersatz. + if flag(examples) + build-depends: + array, + base < 5, + bytestring, + ersatz, + mtl + else + buildable: False + default-language: Haskell2010 + main-is: Synthesis.hs + ghc-options: -Wall -Wno-type-defaults + hs-source-dirs: examples/qbf + -- test-suite properties -- type: exitcode-stdio-1.0 -- ghc-options: -Wall @@ -282,9 +321,8 @@ containers, data-default, ersatz, - HUnit >= 1.2, - test-framework >= 0.6, - test-framework-hunit >= 0.2 + tasty >= 1.4 && < 1.6, + tasty-hunit >= 0.10 && < 0.11 default-language: Haskell2010 ghc-options: -Wall diff --git a/examples/qbf/Coloring.hs b/examples/qbf/Coloring.hs new file mode 100644 --- /dev/null +++ b/examples/qbf/Coloring.hs @@ -0,0 +1,115 @@ +{-# LANGUAGE CPP #-} +module Main where + +import Prelude hiding (not, (&&), and, or) + +import Ersatz +import Ersatz.Relation +import Ersatz.Counting + +import qualified Data.Array as A +import Data.Array (Array, Ix) + +import Control.Monad.State.Lazy (StateT) + +import Data.List (tails) + +import qualified Data.ByteString.Lazy as B +import qualified Data.ByteString.Lazy.Char8 as C +import Data.Functor.Identity +#if !(MIN_VERSION_base(4,11,0)) +import Data.Semigroup (Semigroup(..)) +#endif + +import Options.Applicative +import Text.Printf (printf) + + +data Coloring = Coloring Int Int Int + +coloring :: Parser Coloring +coloring = Coloring + <$> argument auto ( metavar "n" <> showDefault <> value 11 <> help "Number of nodes of graph G" ) + <*> argument auto ( metavar "c" <> showDefault <> value 3 <> help "G is not c-colorable" ) + <*> argument auto ( metavar "k" <> showDefault <> value 3 <> help "G has no complete subgraph with k nodes" ) + +-- | default: Grötzsch graph: not 3-colorable and K3-free (11 nodes) +main :: IO () +main = execParser options >>= run + where options = info (coloring <**> helper) fullDesc + +run :: Coloring -> IO () +run (Coloring n c k) = do + printf "n = %d, c = %d, k = %d\n" n c k + formulaSize $ problem n c k + solve $ problem n c k + + +solve :: StateT QSAT IO (Relation Int Int) -> IO () +solve p = do + result <- solveWith depqbf p + case result of + (Satisfied, Just r) -> mapM_ putStrLn [table r, show $ edgesA r] + _ -> putStrLn "unsat" + +-- | @problem n c k@ generates a QBF problem that encodes a graph with @n@ nodes, +-- which is not @c@-colorable and does not contain a complete subgraph with @k@ nodes. +problem :: Monad a => Int -> Int -> Int -> StateT QSAT a (Relation Int Int) +problem n c k = do + r <- symmetric_relation ((0,0),(n-1,n-1)) + col <- universally_quantified_relation ((0,0),(n-1,c-1)) + assert $ and [ + irreflexive r + , not $ has_k k r + , is_coloring col ==> not $ proper col r + ] + return r + + +universally_quantified_relation :: (Ix a, Ix b, MonadQSAT s m) + => ((a,b),(a,b)) -> m (Relation a b) +universally_quantified_relation bnd = do + pairs <- sequence $ do + p <- A.range bnd + return $ do + x <- forall_ + return (p,x) + return $ build bnd pairs + +-- | @has_k n r@ encodes the constraint that @r@ has a complete subgraph with @n@ nodes. +has_k :: Ix a => Int -> Relation a a -> Bit +has_k n r = or $ do + xss <- select n $ universe r + return $ and $ do + (x:xs) <- tails xss + y <- xs + return $ r!(x,y) + +-- | select 2 [1..4] = [[1,2],[1,3],[1,4],[2,3],[2,4],[3,4]] +select :: Int -> [a] -> [[a]] +select 0 _ = [[]] +select _ [] = [] +select k (x:xs) = map (x:) (select (k-1) xs) ++ select k xs + +-- | Given a relation r with domain a and codomain b, check if r matches every element in a +-- to exactly one element in b. +is_coloring :: Ix a => Relation a a -> Bit +is_coloring c = and $ do + i <- domain c + return $ exactly 1 $ do + j <- codomain c + return $ c!(i,j) + +-- | @proper c r@ encodes the constraint that @c@ is a proper coloring for @r@. +proper :: Ix a => Relation a a -> Relation a a -> Bit +proper col r = and $ do + (p,q) <- indices r + j <- codomain col + return $ r!(p,q) ==> not $ col!(p,j) && col!(q,j) + + +edgesA :: (Ix a, Ix b) => Array (a,b) Bool -> [(a,b)] +edgesA a = [ i | (i, b) <- A.assocs a, b == True] + +formulaSize :: StateT QSAT Identity a -> IO () +formulaSize p = mapM_ C.putStrLn $ take 2 $ B.split 10 $ qdimacsQSAT p diff --git a/examples/qbf/Synthesis.hs b/examples/qbf/Synthesis.hs new file mode 100644 --- /dev/null +++ b/examples/qbf/Synthesis.hs @@ -0,0 +1,91 @@ +-- | An example program that solves a circuit synthesis problem with the Boolean Chain approach, +-- as cited in "Circuit Minimization with QBF-Based Exact Synthesis" by Reichl et al. 2023 +-- . + +module Main where + +import Prelude hiding (not, (&&), and, or, product) + +import Ersatz +import Ersatz.Relation +import Ersatz.Counting + +import qualified Data.Array as A +import Data.Array (Array, Ix) + +import Control.Monad.State.Lazy (StateT) +import Control.Monad (guard) + +import Text.Printf (printf) +import Data.List (sortOn) + +import qualified Data.ByteString.Lazy as B +import qualified Data.ByteString.Lazy.Char8 as C +import Data.Functor.Identity + + +-- | AIG where @atmost 2 [1,2,3,4]@ is equivalent to @10@ +-- +-- Another problem that can be quickly solved is, for example: +-- n = 3, l = 5, m = 1, f xs = [exactly 2 xs] +-- (AIG where @exactly 2 [1,2,3]@ is equivalent to @8@) +main :: IO () +main = do + let n = 4 -- number of inputs + l = 6 -- number of steps (gates) + m = 1 -- number of outputs + f :: [Bit] -> [Bit] + f xs = [atmost 2 xs] + formulaSize $ problem f n l m + solve $ problem f n l m + + +solve :: StateT QSAT IO (Relation Int Int, Relation Int Int) -> IO () +solve p = do + result <- solveWith depqbf p + case result of + (Satisfied, Just (s,o)) -> printf "output: %s\nAIG:\n%s%s\n" (show $ map fst $ sortOn snd $ edgesA o) (table s) (show $ edgesA s) + _ -> putStrLn "unsat" + +-- | @problem f n l m@ generates a QBF problem that encodes an AIG graph with @n@ inputs, +-- @l@ gates and @m@ outputs which is equivalent to the boolean function @f@. +problem :: Monad a => ([Bit] -> [Bit]) -> Int -> Int -> Int -> StateT QSAT a (Relation Int Int, Relation Int Int) +problem f n l m = do + s <- relation ((n+1,1),(n+l,n+l)) -- selection variables: (x,y) is in s iff gate x takes gate/input y as an input + assert $ and $ do -- ensure that s is acyclic (DAG) + (i,j) <- indices s + guard (i <= j) + return $ s!(i,j) === false + o <- relation ((1,1),(n+l,m)) -- output variables: (x,y) is in o iff output y is gate/input x + assert $ regular_in_degree 1 o + v <- universally_quantified_relation ((1,1),(1,n)) -- input variables: (1,y) is in v iff input y is true + g <- relation ((1,1),(1,n+l)) -- gate value variables: (1,y) is in g iff gate/input y is true + assert $ and $ do + i <- [1..n] + return $ g!(1,i) === v!(1,i) + assert $ and $ do -- g!(1,y) = nand xs where xs is the list of inputs of y + i <- [n+1..n+l] + let val = not $ and $ do + p <- [1..i-1] + return $ s!(i,p) ==> g!(1,p) + return $ g!(1,i) === val + assert $ f (elems v) === elems (product g o) + return (s,o) + + +universally_quantified_relation :: (Ix a, Ix b, MonadQSAT s m) + => ((a,b),(a,b)) -> m (Relation a b) +universally_quantified_relation bnd = do + pairs <- sequence $ do + p <- A.range bnd + return $ do + x <- forall_ + return (p,x) + return $ build bnd pairs + + +edgesA :: (Ix a, Ix b) => Array (a,b) Bool -> [(a,b)] +edgesA a = [ i | (i, True) <- A.assocs a] + +formulaSize :: StateT QSAT Identity a -> IO () +formulaSize p = mapM_ C.putStrLn $ take 2 $ B.split 10 $ qdimacsQSAT p diff --git a/src/Ersatz/Bits.hs b/src/Ersatz/Bits.hs --- a/src/Ersatz/Bits.hs +++ b/src/Ersatz/Bits.hs @@ -40,7 +40,7 @@ import Data.Bits ((.&.), (.|.), shiftL, shiftR) import qualified Data.Bits as Data import Data.Foldable (toList) -import Data.List (unfoldr, foldl') +import qualified Data.List as List (unfoldr, foldl') import Data.Stream.Infinite (Stream(..)) import Data.Word (Word8) import Ersatz.Bit @@ -178,7 +178,7 @@ {-# INLINE numToBool #-} boolsToNum :: (Num a, Data.Bits a) => [Bool] -> a -boolsToNum = foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0 +boolsToNum = List.foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0 {-# INLINE boolsToNum #-} boolToNum :: Num a => Bool -> a @@ -284,7 +284,7 @@ -- Integers to Integer return (foldr (\x acc -> x + 2 * acc) 0 zs) - encode = Bits . unfoldr step + encode = Bits . List.unfoldr step where step x = case compare x 0 of diff --git a/src/Ersatz/Problem.hs b/src/Ersatz/Problem.hs --- a/src/Ersatz/Problem.hs +++ b/src/Ersatz/Problem.hs @@ -39,6 +39,8 @@ , QDIMACS(..) , WDIMACS(..) , dimacs, qdimacs, wdimacs + , writeDimacs, writeQdimacs, writeWdimacs + , writeDimacs', writeQdimacs', writeWdimacs' ) where import Data.ByteString.Builder @@ -57,6 +59,7 @@ import Ersatz.Internal.Formula import Ersatz.Internal.Literal import Ersatz.Internal.StableName +import System.IO ( withFile, IOMode(WriteMode) ) import System.IO.Unsafe import Data.Sequence (Seq) import qualified Data.Sequence as Seq @@ -333,3 +336,52 @@ -- Or is this fused away (because of Coercible)? satClauses :: HasSAT s => s -> Seq IntSet satClauses s = fmap clauseSet (formulaSet (s^.formula)) + + +------------------------------------------------------------------------------ +-- Writing SATs +------------------------------------------------------------------------------ + +writeBuilder :: MonadIO m => FilePath -> Builder -> m () +writeBuilder path builder = liftIO $ do + withFile path WriteMode $ \fh -> + hPutBuilder fh builder + +-- | Write a 'DIMACS' problem to a file at a particular path. Useful if you want +-- to experiment with solvers, solver options, or measure effects of different encodings. +-- +-- @writeDimacs path m@ can be used in the same contexts you would call +-- @solveWith solverName m@. +writeDimacs :: (MonadIO m, DIMACS s, Default s) => FilePath -> StateT s m a -> m () +writeDimacs path m = writeDimacs' path . snd =<< runStateT m def + +-- | Write a 'QDIMACS' problem to a file at a particular path. Useful if you want +-- to experiment with solvers, solver options, or measure effects of different encodings. +-- +-- @writeQDimacs path m@ can be used in the same contexts you would call +-- @solveWith solverName m@. +writeQdimacs :: (MonadIO m, QDIMACS s, Default s) => FilePath -> StateT s m a -> m () +writeQdimacs path m = writeQdimacs' path . snd =<< runStateT m def + +-- | Write a 'WDIMACS' problem to a file at a particular path. Useful if you want +-- to experiment with solvers, solver options, or measure effects of different encodings. +-- +-- | @writeWdimacs path m@ can be used in the same contexts you would call +-- @solveWith solverName m@ +writeWdimacs :: (MonadIO m, WDIMACS s, Default s) => FilePath -> StateT s m a -> m () +writeWdimacs path m = writeWdimacs' path . snd =<< runStateT m def + +-- | Write a 'DIMACS' problem to a file at a particular path. Useful if you want +-- to experiment with solvers, solver options, or measure effects of different encodings. +writeDimacs' :: (MonadIO m, DIMACS t) => FilePath -> t -> m () +writeDimacs' path = writeBuilder path . dimacs + +-- | Write a 'QDIMACS' problem to a file at a particular path. Useful if you want +-- to experiment with solvers, solver options, or measure effects of different encodings. +writeQdimacs' :: (MonadIO m, QDIMACS t) => FilePath -> t -> m () +writeQdimacs' path = writeBuilder path . qdimacs + +-- | Write a 'WDIMACS' problem to a file at a particular path. Useful if you want +-- to experiment with solvers, solver options, or measure effects of different encodings. +writeWdimacs' :: (MonadIO m, WDIMACS t) => FilePath -> t -> m () +writeWdimacs' path = writeBuilder path . wdimacs diff --git a/src/Ersatz/Relation.hs b/src/Ersatz/Relation.hs --- a/src/Ersatz/Relation.hs +++ b/src/Ersatz/Relation.hs @@ -9,15 +9,20 @@ -- -- These are rarely needed, because we provide operations and properties -- in a point-free style, that is, without reference to individual indices and elements. +-- +-- Unless otherwise specified, the size of the generated formulas is linear in \( |A| \cdot |B| \), +-- where \(A\) and \(B\) represent the domain and codomain of the involved relation(s). module Ersatz.Relation ( module Ersatz.Relation.Data , module Ersatz.Relation.Op , module Ersatz.Relation.Prop +, module Ersatz.Relation.ARS ) where import Ersatz.Relation.Data import Ersatz.Relation.Op import Ersatz.Relation.Prop +import Ersatz.Relation.ARS diff --git a/src/Ersatz/Relation/ARS.hs b/src/Ersatz/Relation/ARS.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Relation/ARS.hs @@ -0,0 +1,223 @@ +module Ersatz.Relation.ARS ( +-- * Abstract rewriting + terminating, assert_terminating +, peak, valley +, locally_confluent +, confluent, semiconfluent +, convergent, assert_convergent +, point_symmetric +, relative_to +, connected +, is_nf +, nf_property +, unique_nfs, unique_nfs_reduction +) + +where + +import Prelude hiding ( (&&), not, or, and, all, product ) + +import Ersatz.Bit +import Ersatz.Equatable +import Ersatz.Problem ( MonadSAT ) + +import Ersatz.Relation.Data +import Ersatz.Relation.Op +import Ersatz.Relation.Prop + +import Data.Ix +import Control.Monad ( guard ) + + +-- | Tests if a relation \( R \subseteq A \times A \) is terminating, i.e., +-- there is no infinite sequence \( x_1, x_2, ... \) with \( x_i \in A \) +-- such that \( (x_i, x_{i+1}) \in R \) holds. +-- +-- Formula size: linear in \( |A|^3 \) +terminating :: Ix a => Relation a a -> Bit +terminating r = irreflexive $ transitive_closure r + +-- | Monadic version of 'terminating'. +-- +-- Note that @assert_terminating@ cannot be used for expressing non-termination of a relation, +-- only for expressing termination. +-- +-- Formula size: linear in \( |A|^3 \) +-- +-- ==== __Example__ +-- +-- @ +-- example = do +-- result <- 'Ersatz.Solver.solveWith' 'Ersatz.Solver.Minisat.minisat' $ do +-- r <- 'relation' ((0,0),(2,2)) +-- 'Ersatz.Bit.assert' $ 'Ersatz.Counting.atleast' 3 $ 'elems' r +-- 'assert_terminating' r +-- return r +-- case result of +-- (Satisfied, Just r) -> do putStrLn $ 'table' r; return True +-- _ -> return False +-- @ +assert_terminating :: (Ix a, MonadSAT s m) => Relation a a -> m () +assert_terminating r = do + s <- relation $ bounds r + assert $ and [ + transitive s + , irreflexive s + , implies r s ] + +-- | Constructs the peak \( R^{-1} \circ S \) of two relations +-- \( R, S \subseteq A \times A \). +-- +-- Formula size: linear in \( |A|^3 \) +peak :: Ix a => Relation a a -> Relation a a -> Relation a a +peak r = product (mirror r) + +-- | Constructs the valley \( R \circ S^{-1} \) of two relations +-- \( R, S \subseteq A \times A \). +-- +-- Formula size: linear in \( |A|^3 \) +valley :: Ix a => Relation a a -> Relation a a -> Relation a a +valley r s = product r (mirror s) + +-- | Tests if a relation \( R \subseteq A \times A \) is locally confluent, i.e., +-- \( \forall a,b,c \in A: ((a,b) \in R) \land ((a,c) \in R) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \). +-- +-- Formula size: linear in \( |A|^3 \) +locally_confluent :: Ix a => Relation a a -> Bit +locally_confluent r = + let r' = transitive_reflexive_closure r + in implies (peak r r) (valley r' r') + +-- | Tests if a relation \( R \subseteq A \times A \) is confluent, i.e., +-- \( \forall a,b,c \in A: ((a,b) \in R^*) \land ((a,c) \in R^*) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \). +-- +-- Formula size: linear in \( |A|^3 \) +confluent :: Ix a => Relation a a -> Bit +confluent r = + let r' = transitive_reflexive_closure r + in implies (peak r' r') (valley r' r') + +-- | Tests if a relation \( R \subseteq A \times A \) is semi-confluent, i.e., +-- \( \forall a,b,c \in A: ((a,b) \in R) \land ((a,c) \in R^*) \rightarrow \exists d \in A: ((b,d) \in R^*) \land ((c,d)\in R^*) \). +-- +-- @semiconfluent@ is equivalent to 'confluent'. +-- +-- Formula size: linear in \( |A|^3 \) +semiconfluent :: Ix a => Relation a a -> Bit +semiconfluent r = + let r' = transitive_reflexive_closure r + in implies (peak r r') (valley r' r') + +-- | Tests if a relation \( R \subseteq A \times A \) is convergent, i.e., +-- \( R \) is 'terminating' and 'confluent'. +-- +-- Formula size: linear in \( |A|^3 \) +convergent :: Ix a => Relation a a -> Bit +convergent r = and [terminating r, locally_confluent r] + +-- | Monadic version of 'convergent'. +-- +-- Note that @assert_convergent@ cannot be used for expressing non-convergence of a relation, +-- only for expressing convergence. +-- +-- Formula size: linear in \( |A|^3 \) +-- +-- ==== __Example__ +-- +-- @ +-- example = do +-- result <- 'Ersatz.Solver.solveWith' 'Ersatz.Solver.Minisat.minisat' $ do +-- r <- 'relation' ((0,0),(3,3)) +-- 'Ersatz.Bit.assert' $ 'Ersatz.Counting.exactly' 3 $ 'elems' r +-- 'assert_convergent' r +-- 'Ersatz.Bit.assert' $ 'Ersatz.Bit.not' $ 'transitive' r +-- return r +-- case result of +-- (Satisfied, Just r) -> do putStrLn $ 'table' r; return True +-- _ -> return False +-- @ +assert_convergent :: (Ix a, MonadSAT s m) => Relation a a -> m () +assert_convergent r = do + s <- relation $ bounds r + t <- relation $ bounds r + let u = universe r + i = indices r + assert $ and [ + transitive s + , irreflexive s + , implies r s + , all (\x -> is_nf x r ==> t ! (x,x)) u + , all (\(x,y) -> s!(x,y) && t!(y,y) ==> t!(x,y)) i + , nor $ do + (x,y) <- i; z <- u; guard $ y /= z + return $ t ! (x,y) && t ! (x,z) ] + +-- | Tests if the matrix representation (i.e. the array) of a relation +-- \( R \subseteq A \times A \) is point symmetric, i.e., for the matrix representation +-- \( \begin{pmatrix} a_{11} & \dots & a_{1n} \\ \vdots & \ddots & \vdots \\ a_{n1} & \dots & a_{nn} \end{pmatrix} \) +-- holds \( a_{ij} = a_{(n-i+1)(n-j+1)} \). +point_symmetric :: Ix a => Relation a a -> Bit +point_symmetric r + | is_homogeneous r = elems r === reverse (elems r) + | otherwise = error "The domain must equal the codomain!" + +-- | Given two relations \( R, S \subseteq A \times A \), +-- construct \( R \) relative to \( S \) defined by \( R/S = S^* \circ R \circ S^* \). +-- +-- Formula size: linear in \( |A|^3 \) +relative_to :: Ix a => Relation a a -> Relation a a -> Relation a a +r `relative_to` s = + let s' = transitive_reflexive_closure s + in foldl1 product [ s', r , s' ] + +-- | Tests if a relation \( R \subseteq A \times A \) is connected, +-- i.e., \( (R \cup R^{-1})^* = A \times A \). +-- +-- Formula size: linear in \( |A|^3 \) +connected :: Ix a => Relation a a -> Bit +connected r = complete $ equivalence_closure r + +-- | Given an element \( x \in A \) and a relation \( R \subseteq A \times A \), +-- check if \( x \) is a normal form, i.e., \( \forall y \in A: (x,y) \notin R \). +-- +-- Formula size: linear in \( |A| \) +is_nf :: Ix a => a -> Relation a a -> Bit +is_nf x r = + let ((_,b),(_,d)) = bounds r + in nor $ map (r !) $ range ((x,b),(x,d)) + +-- | Tests if a relation \( R \subseteq A \times A \) has the normal form property, +-- i.e., \( \forall a,b \in A \) holds: if \(b\) is a normal form and +-- \( (a,b) \in (R \cup R^{-1})^{*} \), then \( (a,b) \in R^{*} \). +-- +-- Formula size: linear in \( |A|^3 \) +nf_property :: Ix a => Relation a a -> Bit +nf_property r = and $ do + let trc = transitive_reflexive_closure r + ec = equivalence_closure r + (x,y) <- indices r + return $ and [is_nf y r, ec ! (x,y)] ==> trc ! (x,y) + +-- | Tests if a relation \( R \subseteq A \times A \) has the unique normal form property, +-- i.e., \( \forall a,b \in A \) with \( a \neq b \) holds: if \(a\) and \(b\) are normal forms, +-- then \( (a,b) \notin (R \cup R^{-1})^{*} \). +-- +-- Formula size: linear in \( |A|^3 \) +unique_nfs :: Ix a => Relation a a -> Bit +unique_nfs r = and $ do + let ec = equivalence_closure r + (x,y) <- indices r + guard $ x < y + return $ and [is_nf x r, is_nf y r] ==> not $ ec ! (x,y) + +-- | Tests if a relation \( R \subseteq A \times A \) has the unique normal form property +-- with respect to reduction, i.e., \( \forall a,b \in A \) with \( a \neq b \) holds: +-- if \(a\) and \(b\) are normal forms, then \( (a,b) \notin ((R^{*})^{-1} \circ R^{*}) \). +-- +-- Formula size: linear in \( |A|^3 \) +unique_nfs_reduction :: Ix a => Relation a a -> Bit +unique_nfs_reduction r = and $ do + let trc = transitive_reflexive_closure r + (x,y) <- indices r + guard $ x < y + return $ and [is_nf x r, is_nf y r] ==> not $ peak trc trc ! (x,y) diff --git a/src/Ersatz/Relation/Data.hs b/src/Ersatz/Relation/Data.hs --- a/src/Ersatz/Relation/Data.hs +++ b/src/Ersatz/Relation/Data.hs @@ -1,22 +1,27 @@ {-# language TypeFamilies #-} -module Ersatz.Relation.Data ( --- * The 'Relation' type +module Ersatz.Relation.Data ( +-- * The @Relation@ type Relation -- * Construction , relation, symmetric_relation , build -, buildFrom +, buildFrom, buildFromM , identity -- * Components , bounds, (!), indices, assocs, elems --- * +, domain, codomain, universe +, universeSize +, is_homogeneous +, card +-- * Pretty printing , table ) where -import Prelude hiding ( and ) +import Prelude hiding ( and, (&&), any ) import Ersatz.Bit +import Ersatz.Bits ( Bits, sumBit ) import Ersatz.Codec import Ersatz.Variable (exists) import Ersatz.Problem (MonadSAT) @@ -34,18 +39,18 @@ -- so @a@ and @b@ have to be instances of 'Ix', -- and both \(A\) and \(B\) are intervals. -newtype Relation a b = Relation (A.Array (a, b) Bit) +newtype Relation a b = Relation (Array (a, b) Bit) instance (Ix a, Ix b) => Codec (Relation a b) where - type Decoded (Relation a b) = A.Array (a, b) Bool + type Decoded (Relation a b) = Array (a, b) Bool decode s (Relation a) = decode s a encode a = Relation $ encode a -- | @relation ((amin,bmin),(amax,mbax))@ constructs an indeterminate relation \( R \subseteq A \times B \) --- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}$. +-- where \(A\) is @{amin .. amax}@ and \(B\) is @{bmin .. bmax}@. relation :: ( Ix a, Ix b, MonadSAT s m ) => - ((a,b),(a,b)) + ((a,b),(a,b)) -> m ( Relation a b ) relation bnd = do pairs <- sequence $ do @@ -56,12 +61,10 @@ return $ build bnd pairs -- | Constructs an indeterminate relation \( R \subseteq B \times B \) --- that it is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \). --- --- A symmetric relation is an undirected graph, possibly with loops. +-- that is symmetric, i.e., \( \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) \). symmetric_relation :: (MonadSAT s m, Ix b) => - ((b, b), (b, b)) -- ^ Since a symmetric relation must be homogeneous, the domain must equal the codomain. + ((b, b), (b, b)) -- ^ Since a symmetric relation must be homogeneous, the domain must equal the codomain. -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@. -> m (Relation b b) symmetric_relation bnd = do @@ -75,12 +78,12 @@ return $ build bnd $ concat pairs -- | Constructs a relation \(R \subseteq A \times B \) from a list. --- +-- -- ==== __Example__ -- -- @ --- r = build ((0,'a'),(1,'b')) [((0,'a'), true), ((0,'b'), false), --- ((1,'a'), false), ((1,'b'), true))] +-- r = build ((0,'a'),(1,'b')) [ ((0,'a'), true), ((0,'b'), false) +-- , ((1,'a'), false), ((1,'b'), true) ] -- @ build :: ( Ix a, Ix b ) => ((a,b),(a,b)) @@ -92,48 +95,63 @@ -- | Constructs a relation \(R \subseteq A \times B \) from a function. buildFrom :: (Ix a, Ix b) - => (a -> b -> Bit) -- ^ A function with the specified signature, that assigns a 'Bit'-value - -- to each element \( (x,y) \in A \times B \). - -> ((a,b),(a,b)) + => ((a,b),(a,b)) + -> ((a,b) -> Bit) -- ^ A function that assigns a 'Bit'-value + -- to each element \( (x,y) \in A \times B \). -> Relation a b -buildFrom p bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) -> ((i, j), p i j) +buildFrom bnd p = build bnd $ flip map (A.range bnd) $ \ i -> (i, p i) --- | Constructs the identity relation \(I \subseteq A \times A, I = \{ (x,x) ~|~ x \in A \} \). +-- | Constructs an indeterminate relation \(R \subseteq A \times B\) from a function. +buildFromM :: (Ix a, Ix b, MonadSAT s m) + => ((a,b),(a,b)) + -> ((a,b) -> m Bit) + -> m (Relation a b) +buildFromM bnd p = do + pairs <- sequence $ do + i <- A.range bnd + return $ do + x <- p i + return (i, x) + return $ build bnd pairs + +-- | Constructs the identity relation \(I = \{ (x,x) ~|~ x \in A \} \subseteq A \times A\). identity :: (Ix a) - => ((a,a),(a,a)) -- ^ Since the identity relation is homogeneous, the domain must equal the codomain. + => ((a,a),(a,a)) -- ^ Since the identity relation is homogeneous, the domain must equal the codomain. -- Therefore, given bounds @((p,q),(r,s))@, it must hold that @p=q@ and @r=s@. -> Relation a a -identity = buildFrom (\ i j -> bool $ i == j) +identity ((a,b),(c,d)) + | (a,c) == (b,d) = buildFrom ((a,b),(c,d)) (\ (i,j) -> bool $ i == j) + | otherwise = error "The domain must equal the codomain!" -- | The bounds of the array that correspond to the matrix representation of the given relation. -- -- ==== __Example__ -- --- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))] +-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)] -- >>> bounds r -- ((0,0),(1,1)) bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b)) bounds ( Relation r ) = A.bounds r --- | The list of indices, where each index represents an element \( (x,y) \in A \times B \) +-- | The list of indices, where each index represents an element \( (x,y) \in A \times B \) -- that may be contained in the given relation \(R \subseteq A \times B \). -- -- ==== __Example__ -- --- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))] +-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)] -- >>> indices r -- [(0,0),(0,1),(1,0),(1,1)] indices :: (Ix a, Ix b) => Relation a b -> [(a, b)] indices ( Relation r ) = A.indices r --- | The list of tuples for the given relation \(R \subseteq A \times B \), --- where the first element represents an element \( (x,y) \in A \times B \) +-- | The list of tuples for the given relation \(R \subseteq A \times B \), +-- where the first element represents an element \( (x,y) \in A \times B \) -- and the second element indicates via a 'Bit' , if \( (x,y) \in R \) or not. --- +-- -- ==== __Example__ -- --- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))] +-- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false)] -- >>> assocs r -- [((0,0),Var (-1)),((0,1),Var 1),((1,0),Var 1),((1,1),Var (-1))] assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)] @@ -150,10 +168,10 @@ elems :: (Ix a, Ix b) => Relation a b -> [Bit] elems ( Relation r ) = A.elems r --- | The 'Bit'-value for a given element \( (x,y) \in A \times B \) +-- | The 'Bit'-value for a given element \( (x,y) \in A \times B \) -- and a given relation \(R \subseteq A \times B \) that indicates -- if \( (x,y) \in R \) or not. --- +-- -- ==== __Example__ -- -- >>> r = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))] @@ -164,17 +182,50 @@ (!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit Relation r ! p = r A.! p +-- | The domain \(A\) of a relation \(R \subseteq A \times B\). +domain :: (Ix a, Ix b) => Relation a b -> [a] +domain r = + let ((x,_),(x',_)) = bounds r + in A.range (x,x') + +-- | The codomain \(B\) of a relation \(R \subseteq A \times B\). +codomain :: (Ix a, Ix b) => Relation a b -> [b] +codomain r = + let ((_,y),(_,y')) = bounds r + in A.range (y,y') + +-- | The universe \(A\) of a relation \(R \subseteq A \times A\). +universe :: Ix a => Relation a a -> [a] +universe r + | is_homogeneous r = domain r + | otherwise = error "Relation is not homogeneous!" + +-- | The size of the universe \(A\) of a relation \(R \subseteq A \times A\). +universeSize :: Ix a => Relation a a -> Int +universeSize r + | is_homogeneous r = + let ((a,_),(c,_)) = bounds r + in A.rangeSize (a,c) + | otherwise = error "Relation is not homogeneous!" + +-- | Tests if a relation is homogeneous, i.e., if the domain is equal to the codomain. +is_homogeneous :: Ix a => Relation a a -> Bool +is_homogeneous r = + let ((a,b),(c,d)) = bounds r + in (a == b) && (c == d) + +-- | The number of pairs \( (x,y) \in R \) for the given relation +-- \( R \subseteq A \times B \). +card :: (Ix a, Ix b) => Relation a b -> Bits +card = sumBit . elems + -- | Print a satisfying assignment from a SAT solver, where the assignment is interpreted as a relation. -- @putStrLn $ table \@ corresponds to the matrix representation of this relation. -table :: (Enum a, Ix a, Enum b, Ix b) +table :: (Ix a, Ix b) => Array (a,b) Bool -> String table r = unlines $ do let ((a,b),(c,d)) = A.bounds r - x <- [ a .. c ] + x <- A.range (a,c) return $ unwords $ do - y <- [ b .. d ] + y <- A.range (b,d) return $ if r A.! (x,y) then "*" else "." - - - - diff --git a/src/Ersatz/Relation/Op.hs b/src/Ersatz/Relation/Op.hs --- a/src/Ersatz/Relation/Op.hs +++ b/src/Ersatz/Relation/Op.hs @@ -2,7 +2,7 @@ module Ersatz.Relation.Op -( +( -- * Operations mirror , union @@ -12,76 +12,79 @@ , intersection , reflexive_closure , symmetric_closure +, transitive_closure +, transitive_reflexive_closure +, equivalence_closure ) where import Ersatz.Relation.Data -import Prelude hiding ( and, or, not, product ) -import Ersatz.Bit (and, or, not) +import Prelude hiding ( (&&), (||), and, or, not, product ) +import Ersatz.Bit +import qualified Data.Array as A import Data.Ix --- | Constructs the converse relation \( R^{-1} \subseteq B \times A \) of a relation --- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \). +-- | Constructs the converse relation \( R^{-1} \) of a relation +-- \( R \subseteq A \times B \), which is defined by \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \subseteq B \times A \). mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a mirror r = let ((a,b),(c,d)) = bounds r in build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y)) --- | Constructs the complement relation \( \overline{R} \) --- of a relation \( R \subseteq A \times B \), which is defined by +-- | Constructs the complement relation \( \overline{R} \) +-- of a relation \( R \subseteq A \times B \), which is defined by -- \( \overline{R} = \{ (x,y) \in A \times B ~|~ (x,y) \notin R \} \). complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b complement r = build (bounds r) $ do i <- indices r ; return ( i, not $ r!i ) --- | Constructs the difference \( R \setminus S \) of the relations --- \(R\) and \(S\), that contains all elements that are in \(R\) but not in \(S\), i.e., +-- | Constructs the difference \( R \setminus S \) of the relations +-- \(R, S \subseteq A \times B \), that contains all elements that are in \(R\) but not in \(S\), i.e., -- \( R \setminus S = \{ (x,y) \in R ~|~ (x,y) \notin S \} \). --- --- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \), --- then \( A \times B \) must be a subset of \( C \times D \) and --- \( R \setminus S \subseteq A \times B \). difference :: ( Ix a , Ix b ) => Relation a b -> Relation a b -> Relation a b difference r s = intersection r $ complement s --- | Constructs the union \( R \cup S \) of the relations \( R \) and \( S \). --- --- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \), --- it must hold that \( A \times B \subseteq C \times D \). +-- | Constructs the union \( R \cup S \) of the relations \( R, S \subseteq A \times B \). union :: ( Ix a , Ix b ) - => Relation a b -> Relation a b -> Relation a b -union r s = build ( bounds r ) $ do - i <- indices r - return (i, or [ r!i, s!i ] ) + => Relation a b -> Relation a b -> Relation a b +union r s + | bounds r == bounds s = build ( bounds r ) $ do + i <- indices r + return (i, r!i || s!i) + | otherwise = error "Relations don't have the same bounds!" --- | Constructs the composition \( R \cdot S \) of the relations --- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is --- defined by \( R \cdot S = \{ (a,c) ~|~ ((a,b) \in R) \land ((b,c) \in S) \} \). +-- | Constructs the composition \( R \circ S \) of the relations +-- \( R \subseteq A \times B \) and \( S \subseteq B \times C \), which is +-- defined by \( R \circ S = \{ (a,c) ~|~ (a,b) \in R \land (b,c) \in S \} \). +-- +-- Formula size: linear in \(|A|\cdot|B|\cdot|C|\) product :: ( Ix a , Ix b, Ix c ) - => Relation a b -> Relation b c -> Relation a c + => Relation a b -> Relation b c -> Relation a c product a b = let ((ao,al),(au,ar)) = bounds a - ((_ ,bl),(_ ,br)) = bounds b + ((bo,bl),(bu,br)) = bounds b bnd = ((ao,bl),(au,br)) - in build bnd $ do - i@(x,z) <- range bnd - return (i, or $ do - y <- range ( al, ar ) - return $ and [ a!(x,y), b!(y,z) ] - ) + in if (al,ar) == (bo,bu) + then build bnd $ do + i@(x,z) <- range bnd + return (i, or $ do + y <- range ( al, ar ) + return $ and [ a!(x,y), b!(y,z) ] + ) + else error "Codomain of first relation must equal domain of second relation!" -- | Constructs the relation \( R^{n} \) that results if a relation -- \( R \subseteq A \times A \) is composed \(n\) times with itself. -- --- \( R^{0} \) is the identity relation \( I_{R} = \{ (x,x) ~|~ x \in A \} \) of \(R\). -power :: ( Ix a ) - => Int -- ^ \(n\) - -> Relation a a -> Relation a a +-- \( R^{0} \) is the identity relation \( I = \{ (x,x) ~|~ x \in A \} \). +-- +-- Formula size: linear in \( |A|^3 \cdot \log n \) +power :: ( Ix a ) => Int -> Relation a a -> Relation a a power 0 r = identity ( bounds r ) power 1 r = r power e r = @@ -92,27 +95,58 @@ 0 -> s2 _ -> product s2 r --- | Constructs the intersection \( R \cap S \) of the relations \( R \) and \( S \). --- --- Note that for \( R \subseteq A \times B \) and \( S \subseteq C \times D \), --- it must hold that \( A \times B \subseteq C \times D \). -intersection :: ( Ix a , Ix b) +-- | Constructs the intersection \( R \cap S \) of the relations \( R, S \subseteq A \times B \). +intersection :: ( Ix a , Ix b ) => Relation a b -> Relation a b -> Relation a b -intersection r s = build ( bounds r ) $ do +intersection r s + | bounds r == bounds s = build ( bounds r ) $ do i <- indices r return (i, and [ r!i, s!i ] ) + | otherwise = error "Relations don't have the same bounds!" --- | Constructs the reflexive closure \( R \cup I_{R} \) of the relation --- \( R \subseteq A \times A \), where \( I_{R} = \{ (x,x) ~|~ x \in A \} \) --- is the identity relation of \(R\). +-- | Constructs the reflexive closure \( R \cup R^{0} \) of the relation +-- \( R \subseteq A \times A \). reflexive_closure :: Ix a => Relation a a -> Relation a a reflexive_closure t = union t $ identity $ bounds t --- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation --- \( R \subseteq A \times A \), where \( R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} \) --- is converse relation of \(R\). +-- | Constructs the symmetric closure \( R \cup R^{-1} \) of the relation +-- \( R \subseteq A \times A \). symmetric_closure :: Ix a => Relation a a -> Relation a a symmetric_closure r = union r $ mirror r + +-- | Constructs the transitive closure \( R^{+} \) of the relation +-- \( R \subseteq A \times A \), which is defined by +-- \( R^{+} = \bigcup^{\infty}_{i = 1} R^{i} \). +-- +-- Formula size: linear in \( |A|^3 \) +transitive_closure :: Ix a => Relation a a -> Relation a a +transitive_closure r = + let n = universeSize r + -- @a' ! (0,p,q)@ is true if and only if @r ! (p,q)@ is true + a' = A.listArray ((0,1,1),(n,n,n)) (elems r) + -- @a ! (0,p,q)@ is true if and only if @a' ! (0,p,q)@ is true + a = a' A.// do + -- If x > 0, then @a ! (p,x,q)@ is true if and only if there is a path from p to q via nodes {1,...,x} in r + i@(x,p,q) <- A.range ((1,1,1),(n,n,n)) + return (i, a A.! (x-1,p,q) || a A.! (x-1,p,x) && a A.! (x-1,x,q)) + in build (bounds r) $ zip (indices r) [a A.! i | i <- A.range ((n,1,1),(n,n,n))] + +-- | Constructs the transitive reflexive closure \( R^{*} \) of the relation +-- \( R \subseteq A \times A \), which is defined by +-- \( R^{*} = \bigcup^{\infty}_{i = 0} R^{i} \). +-- +-- Formula size: linear in \( |A|^3 \) +transitive_reflexive_closure :: Ix a => Relation a a -> Relation a a +transitive_reflexive_closure r = + union (transitive_closure r) (identity $ bounds r) + +-- | Constructs the equivalence closure \( (R \cup R^{-1})^* \) of the relation +-- \( R \subseteq A \times A \). +-- +-- Formula size: linear in \( |A|^3 \) +equivalence_closure :: Ix a => Relation a a -> Relation a a +equivalence_closure r = + transitive_reflexive_closure $ symmetric_closure r diff --git a/src/Ersatz/Relation/Prop.hs b/src/Ersatz/Relation/Prop.hs --- a/src/Ersatz/Relation/Prop.hs +++ b/src/Ersatz/Relation/Prop.hs @@ -1,6 +1,7 @@ +{-# OPTIONS_GHC -Wno-orphans #-} module Ersatz.Relation.Prop -( +( -- * Properties implies , symmetric @@ -19,7 +20,6 @@ , complete , total , disjoint -, equals ) where @@ -29,19 +29,23 @@ import Ersatz.Relation.Data import Ersatz.Relation.Op import Ersatz.Counting +import Ersatz.Equatable import Data.Ix --- | Tests if the first relation \(R\) is a subset of the second relation \(S\), --- i.e., every element that is contained in \(R\) is also contained in \(S\). --- --- Note that if \( R \subseteq A \times B \) and \( S \subseteq C \times D \), --- then \( A \times B \) must be a subset of \( C \times D \). + +instance (Ix a, Ix b) => Equatable (Relation a b) where + r === s = and [implies r s, implies s r] + r /== s = not $ r === s + +-- | Given two relations \( R, S \subseteq A \times B \), check if \(R\) is a subset of \(S\). implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> Bit -implies r s = and $ do - i <- indices r - return $ or [ not $ r ! i, s ! i ] +implies r s + | bounds r == bounds s = and $ do + i <- indices r + return $ (r ! i) ==> (s ! i) + | otherwise = error "Relations don't have the same bounds!" -- | Tests if a relation is empty, i.e., the relation doesn't contain any elements. empty :: ( Ix a, Ix b ) @@ -56,46 +60,35 @@ complete r = empty $ complement r -- | Tests if a relation \( R \subseteq A \times A \) is strongly connected, i.e., --- \( \forall x, y \in A: ((x,y) \in R) \lor ((y,x) \in R) \). -total :: ( Ix a) => Relation a a -> Bit +-- \( R \cup R^{-1} = A \times A \). +total :: ( Ix a ) => Relation a a -> Bit total r = complete $ symmetric_closure r --- | Tests if two relations are disjoint, i.e., +-- | Tests if two relations are disjoint, i.e., -- there is no element that is contained in both relations. disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit disjoint r s = empty $ intersection r s --- | Tests if two relations \( R, S \subseteq A \times B \) are equal, --- i.e., they contain the same elements. -equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit -equals r s = and [implies r s, implies s r] - -- | Tests if a relation \( R \subseteq A \times A \) is symmetric, --- i.e., \( \forall x, y \in A: ((x,y) \in R) \rightarrow ((y,x) \in R) \). -symmetric :: ( Ix a) => Relation a a -> Bit +-- i.e., \( R \cup R^{-1} = R \). +symmetric :: ( Ix a ) => Relation a a -> Bit symmetric r = implies r ( mirror r ) -- | Tests if a relation \( R \subseteq A \times A \) is antisymmetric, --- i.e., \( \forall x, y \in A: ((x,y) \in R) \land ((y,x) \in R)) \rightarrow (x = y) \). -anti_symmetric :: ( Ix a) => Relation a a -> Bit +-- i.e., \( R \cap R^{-1} \subseteq R^{0} \). +anti_symmetric :: ( Ix a ) => Relation a a -> Bit anti_symmetric r = implies (intersection r (mirror r)) (identity (bounds r)) -- | Tests if a relation \( R \subseteq A \times A \) is irreflexive, i.e., --- \( \forall x \in A: (x,x) \notin R \). +-- \( R \cap R^{0} = \emptyset \). irreflexive :: ( Ix a ) => Relation a a -> Bit -irreflexive r = and $ do - let ((a,_),(c,_)) = bounds r - x <- range (a, c) - return $ not $ r ! (x,x) +irreflexive r = empty $ intersection (identity $ bounds r) r -- | Tests if a relation \( R \subseteq A \times A \) is reflexive, i.e., --- \( \forall x \in A: (x,x) \in R \). +-- \( R^{0} \subseteq R \). reflexive :: ( Ix a ) => Relation a a -> Bit -reflexive r = and $ do - let ((a,_),(c,_)) = bounds r - x <- range (a,c) - return $ r ! (x,x) +reflexive r = implies (identity $ bounds r) r -- | Given an 'Int' \( n \) and a relation \( R \subseteq A \times B \), check if -- \( \forall x \in A: | \{ (x,y) \in R \} | = n \) and @@ -146,7 +139,9 @@ return $ r ! (x,y) -- | Tests if a relation \( R \subseteq A \times A \) is transitive, i.e., --- \( \forall x, y \in A: ((x,y) \in R) \land ((y,z) \in R) \rightarrow ((x,z) \in R) \). +-- \( R \circ R = R \). +-- +-- Formula size: linear in \( |A|^3 \) transitive :: ( Ix a ) => Relation a a -> Bit transitive r = implies (product r r) r diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs --- a/src/Ersatz/Solver.hs +++ b/src/Ersatz/Solver.hs @@ -9,6 +9,8 @@ -------------------------------------------------------------------- module Ersatz.Solver ( module Ersatz.Solver.DepQBF + , module Ersatz.Solver.Kissat + , module Ersatz.Solver.Lingeling , module Ersatz.Solver.Minisat , module Ersatz.Solver.Z3 , solveWith @@ -20,6 +22,8 @@ import Ersatz.Problem import Ersatz.Solution import Ersatz.Solver.DepQBF +import Ersatz.Solver.Kissat +import Ersatz.Solver.Lingeling import Ersatz.Solver.Minisat import Ersatz.Solver.Z3 diff --git a/src/Ersatz/Solver/DepQBF.hs b/src/Ersatz/Solver/DepQBF.hs --- a/src/Ersatz/Solver/DepQBF.hs +++ b/src/Ersatz/Solver/DepQBF.hs @@ -12,16 +12,18 @@ module Ersatz.Solver.DepQBF ( depqbf , depqbfPath + , depqbfPathArgs ) where -import Data.ByteString.Builder import Control.Monad.IO.Class -import Ersatz.Problem +import Data.Version (Version, makeVersion, parseVersion) +import Ersatz.Problem ( QSAT, writeQdimacs' ) import Ersatz.Solution import Ersatz.Solver.Common import qualified Data.IntMap as I -import System.IO +import System.Exit (ExitCode(..)) import System.Process (readProcessWithExitCode) +import qualified Text.ParserCombinators.ReadP as P -- | This is a 'Solver' for 'QSAT' problems that runs the @depqbf@ solver using -- the current @PATH@, it tries to run an executable named @depqbf@. @@ -36,10 +38,14 @@ -- http://www.qbflib.org/qdimacs.html#output parseOutput :: String -> [(Int, Bool)] parseOutput out = - case lines out of + case filter (not . comment) $ lines out of (_preamble:certLines) -> map parseCertLine certLines [] -> error "QDIMACS output without preamble" where + comment [] = True + comment ('c' : _) = True + comment _ = False + parseCertLine :: String -> (Int, Bool) parseCertLine certLine = case words certLine of @@ -47,14 +53,29 @@ _ -> error $ "Malformed QDIMACS certificate line: " ++ certLine -- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable. +-- This passes different arguments to @depqbf@ depending on its version: +-- +-- * If using version 6.03 or later, this passes @[\"--qdo\", \"--no-dynamic-nenofex\"]@. +-- +-- * Otherwise, this passes @[\"--qdo\"]@. depqbfPath :: MonadIO m => FilePath -> Solver QSAT m -depqbfPath path problem = liftIO $ +depqbfPath path problem = do + ver <- liftIO $ depqbfVersion path + let args | ver >= makeVersion [6,03] + = [ "--qdo", "--no-dynamic-nenofex" ] + | otherwise + = [ "--qdo" ] + depqbfPathArgs path args problem + +-- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable +-- as well as a list of command line arguments. They will appear after the problem file name. +depqbfPathArgs :: MonadIO m => FilePath -> [String] -> Solver QSAT m +depqbfPathArgs path args problem = liftIO $ withTempFiles ".cnf" "" $ \problemPath _ -> do - withFile problemPath WriteMode $ \fh -> - hPutBuilder fh (qdimacs problem) + writeQdimacs' problemPath problem (exit, out, _err) <- - readProcessWithExitCode path [problemPath, "--qdo"] [] + readProcessWithExitCode path (problemPath : args) [] let result = resultOf exit @@ -64,3 +85,56 @@ I.fromList $ parseOutput out _ -> I.empty + +-- | Query @depqbf@'s 'Version' by invoking @depqbf --version@ and parsing the +-- output. This assumes that the output can be parsed as a valid 'Version' and +-- that @depqbf@ versions increase in a way that is compatible with the +-- 'Ord Version' instance (see 'depqbfPath', which compares 'Version's using +-- ('>=')). +depqbfVersion :: FilePath -> IO Version +depqbfVersion path = do + (exit, out, err) <- + readProcessWithExitCode path ["--version"] [] + + let parseError reason = + fail $ unlines + [ "Could not query depqbf version (" ++ reason ++ ")" + , "Standard output:" + , out + , "" + , "Standard error:" + , err + ] + + case exit of + ExitSuccess -> do + -- Should be something like "DepQBF 6.03" + verStrLine <- + case lines err of + line:_ -> pure line + [] -> parseError "no lines of standard error" + -- Should be something like "6.03" + verStr <- + case words verStrLine of + _depQBF:ver:_ -> pure ver + _ -> parseError $ "unexpected version number " ++ verStrLine + -- Convert the string to a full Version + case readEitherP parseVersion verStr of + Left reason -> parseError reason + Right v -> pure v + ExitFailure i -> + parseError $ "exit code " ++ show i ++ ")" + +-- | Like @readEither@ from "Text.Read", but accepting an arbitrary 'P.ReadP' +-- argument instead of requiring a 'Read' constraint. +readEitherP :: P.ReadP a -> String -> Either String a +readEitherP rp s = + case [ x | (x,"") <- P.readP_to_S read' s ] of + [x] -> Right x + [] -> Left "no parse" + _ -> Left "ambiguous parse" + where + read' = do + x <- rp + P.skipSpaces + pure x diff --git a/src/Ersatz/Solver/Kissat.hs b/src/Ersatz/Solver/Kissat.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Solver/Kissat.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Ersatz.Solver.Kissat + ( kissat + , kissatPath + ) where + +import Control.Monad.IO.Class + ( MonadIO ( liftIO + ) + ) +import Ersatz.Problem + ( SAT + , writeDimacs' + ) +import Ersatz.Solution + ( Solver + ) +import Ersatz.Solver.Common + ( resultOf + , withTempFiles + , parseSolution5 + ) +import System.Process + ( readProcessWithExitCode + ) + + +-- | 'Solver' for 'SAT' problems that tries to invoke the @kissat@ executable +-- from the @PATH@. +kissat :: MonadIO m => Solver SAT m +kissat = kissatPath "kissat" + +-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes +-- @kissat@ compatible arguments. +-- +-- The 'FilePath' refers to the path to the executable. +kissatPath :: MonadIO m => FilePath -> Solver SAT m +kissatPath path problem = liftIO $ + withTempFiles ".cnf" "" $ \problemPath _ -> do + writeDimacs' problemPath problem + + (exit, out, _err) <- + readProcessWithExitCode path + [problemPath] + [] + + let sol = parseSolution5 out + + return (resultOf exit, sol) diff --git a/src/Ersatz/Solver/Lingeling.hs b/src/Ersatz/Solver/Lingeling.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Solver/Lingeling.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Ersatz.Solver.Lingeling + ( lingeling + , plingeling + , treengeling + , lingelingPath + , plingelingPath + , treengelingPath + ) where + +import Control.Monad.IO.Class + ( MonadIO ( liftIO + ) + ) +import Ersatz.Problem + ( SAT + , writeDimacs' + ) +import Ersatz.Solution + ( Solver + ) +import Ersatz.Solver.Common + ( resultOf + , withTempFiles + , parseSolution5 + ) +import System.Process + ( readProcessWithExitCode + ) + +-- | 'Solver' for 'SAT' problems that tries to invoke the @lingeling@ executable +-- from the @PATH@. +lingeling :: MonadIO m => Solver SAT m +lingeling = lingelingPath "lingeling" + +-- | 'Solver' for 'SAT' problems that tries to invoke the @plingeling@ executable +-- from the @PATH@. +plingeling :: MonadIO m => Solver SAT m +plingeling = ngelingPath "plingeling" + +-- | 'Solver' for 'SAT' problems that tries to invoke the @treengeling@ executable +-- from the @PATH@. +treengeling :: MonadIO m => Solver SAT m +treengeling = ngelingPath "treengeling" + +-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes +-- @lingeling@ compatible arguments. +-- +-- The 'FilePath' refers to the path to the executable. +lingelingPath :: MonadIO m => FilePath -> Solver SAT m +lingelingPath = ngelingPath + +-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes +-- @plingeling@ compatible arguments. +-- +-- The 'FilePath' refers to the path to the executable. +plingelingPath :: MonadIO m => FilePath -> Solver SAT m +plingelingPath = ngelingPath + +-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes +-- @treengeling@ compatible arguments. +-- +-- The 'FilePath' refers to the path to the executable. +treengelingPath :: MonadIO m => FilePath -> Solver SAT m +treengelingPath = ngelingPath + +-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes +-- @*ngeling@ compatible arguments. +-- +-- The 'FilePath' refers to the path to the executable. +ngelingPath :: MonadIO m => FilePath -> Solver SAT m +ngelingPath path problem = liftIO $ + withTempFiles ".cnf" "" $ \problemPath _ -> do + writeDimacs' problemPath problem + + (exit, out, _err) <- + readProcessWithExitCode path + [problemPath] + [] + + let sol = parseSolution5 out + + return (resultOf exit, sol) diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs --- a/src/Ersatz/Solver/Minisat.hs +++ b/src/Ersatz/Solver/Minisat.hs @@ -19,19 +19,17 @@ , anyminisat ) where -import Data.ByteString.Builder import Control.Exception (IOException, handle) import Control.Monad.IO.Class import Data.IntMap (IntMap) -import Ersatz.Problem +import Ersatz.Problem ( SAT, writeDimacs' ) import Ersatz.Solution import Ersatz.Solver.Common import qualified Data.IntMap.Strict as IntMap -import System.IO import System.Process (readProcessWithExitCode) import qualified Data.ByteString.Char8 as B -import Data.List ( foldl' ) +import qualified Data.List as List ( foldl' ) -- | Hybrid 'Solver' that tries to use: 'cryptominisat5', 'cryptominisat', and 'minisat' anyminisat :: Solver SAT IO @@ -51,8 +49,7 @@ minisatPath :: MonadIO m => FilePath -> Solver SAT m minisatPath path problem = liftIO $ withTempFiles ".cnf" "" $ \problemPath solutionPath -> do - withFile problemPath WriteMode $ \fh -> - hPutBuilder fh (dimacs problem) + writeDimacs' problemPath problem (exit, _out, _err) <- readProcessWithExitCode path [problemPath, solutionPath] [] @@ -71,7 +68,8 @@ parseSolution s = case B.words s of x : ys | x == "SAT" -> - foldl' ( \ m y -> case B.readInt y of + List.foldl' + ( \ m y -> case B.readInt y of Just (v,_) -> if 0 == v then m else IntMap.insert (abs v) (v>0) m Nothing -> error $ "parseSolution: Expected an Int, received " ++ show y ) IntMap.empty ys @@ -87,8 +85,7 @@ cryptominisat5Path :: MonadIO m => FilePath -> Solver SAT m cryptominisat5Path path problem = liftIO $ withTempFiles ".cnf" "" $ \problemPath _ -> do - withFile problemPath WriteMode $ \fh -> - hPutBuilder fh (dimacs problem) + writeDimacs' problemPath problem (exit, out, _err) <- readProcessWithExitCode path [problemPath] [] diff --git a/src/Ersatz/Solver/Z3.hs b/src/Ersatz/Solver/Z3.hs --- a/src/Ersatz/Solver/Z3.hs +++ b/src/Ersatz/Solver/Z3.hs @@ -12,12 +12,10 @@ , z3Path ) where -import Data.ByteString.Builder import Control.Monad.IO.Class -import Ersatz.Problem +import Ersatz.Problem ( SAT, writeDimacs' ) import Ersatz.Solution import Ersatz.Solver.Common -import System.IO import System.Process (readProcessWithExitCode) -- | 'Solver' for 'SAT' problems that tries to invoke the @z3@ executable from the @PATH@ @@ -30,8 +28,7 @@ z3Path :: MonadIO m => FilePath -> Solver SAT m z3Path path problem = liftIO $ withTempFiles ".cnf" "" $ \problemPath _ -> do - withFile problemPath WriteMode $ \fh -> - hPutBuilder fh (dimacs problem) + writeDimacs' problemPath problem (_exit, out, _err) <- readProcessWithExitCode path ["-dimacs", problemPath] [] diff --git a/tests/HUnit.hs b/tests/HUnit.hs --- a/tests/HUnit.hs +++ b/tests/HUnit.hs @@ -6,9 +6,8 @@ import Data.Default import qualified Data.IntMap.Strict as IntMap -import Test.Framework -import Test.Framework.Providers.HUnit -import Test.HUnit (Assertion, (@?=)) +import Test.Tasty (TestTree, defaultMain, testGroup) +import Test.Tasty.HUnit (Assertion, (@?=), testCase) import Ersatz import Ersatz.Internal.Literal @@ -16,12 +15,11 @@ main :: IO () main = defaultMain tests -tests :: [Test] +tests :: TestTree tests = - [ testGroup "unit tests" - [ testCase "unconstrained literals" case_unconstrained_literals - ] - ] + testGroup "unit tests" + [ testCase "unconstrained literals" case_unconstrained_literals + ] -- A regression test for #60 and #76. case_unconstrained_literals :: Assertion diff --git a/tests/Moore.hs b/tests/Moore.hs --- a/tests/Moore.hs +++ b/tests/Moore.hs @@ -1,4 +1,4 @@ --- | graphs n nodes of degree <= d and diameter <= k +-- | graphs n nodes of degree <= d and diameter <= k -- see http://combinatoricswiki.org/wiki/The_Degree_Diameter_Problem_for_General_Graphs -- usage: ./Moore d k n [s] @@ -9,7 +9,7 @@ -- s smaller => faster (more symmetries) but may lose solutions -- test cases: 3 2 10 2 -- petersen graph --- 5 2 24 +-- 5 2 24 {-# language FlexibleContexts #-} @@ -39,7 +39,7 @@ putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ] (s, mg) <- solveWith anyminisat $ moore d k n s case (s, mg) of - (Satisfied, Just g) -> do printA g ; return True + (Satisfied, Just g) -> do putStrLn $ R.table g ; return True _ -> do return False moore :: @@ -50,11 +50,11 @@ -- g <- R.symmetric_relation ((0,0),(n-1,n-1)) g <- periodic_relation s ((0,0),(n-1,n-1)) assert $ R.symmetric g - assert $ R.reflexive g - assert $ R.max_in_degree (d+1) g - assert $ R.max_out_degree (d+1) g + assert $ R.reflexive g + assert $ R.max_in_degree (d+1) g + assert $ R.max_out_degree (d+1) g let p = R.power k g - assert $ R.complete p + assert $ R.complete p return g periodic_relation s bnd = do @@ -65,14 +65,4 @@ return $ R.build bnd $ do i <- A.range bnd return (i, r R.! normal i) - --- | FIXME: this needs to go into a library -printA :: A.Array (Int,Int) Bool -> IO () -printA a = putStrLn $ unlines $ do - let ((u,l),(o,r)) = A.bounds a - x <- [u .. o] - return $ unwords $ do - y <- [ l ..r ] - return $ case a A.! (x,y) of - True -> "* " ; False -> ". "