Safe Haskell	Safe

Data.Algorithm.SatSolver.Fml

Contents

type
constructing
testing
querying
Transforming

Synopsis

newtype Fml a = Fml {
- getClauses :: [Clause a]
}
mk :: Ord a => [Clause a] -> Fml a
(/++/) :: Ord a => Fml a -> Fml a -> Fml a
isEmpty :: Fml a -> Bool
isSatisfied :: Fml a -> Bool
hasUnsatisfiedClause :: Fml a -> Bool
getLits :: Fml a -> [Lit a]
getVars :: Ord a => Fml a -> [Var a]
getUnitClauses :: Ord a => Fml a -> [Clause a]
size :: Fml a -> Int
selectMostFrequentLit :: Ord a => Fml a -> Maybe (Lit a)
selectMonotoneLit :: Ord a => Fml a -> Maybe (Lit a)
toNormal :: (Ord a, Ord b, Num b, Enum b) => Fml a -> Fml b
toDIMACSString :: Ord a => Fml a -> String

type

newtype Fml a Source #

Fml type

Constructors

Fml
Fields getClauses :: [Clause a]

Instances

Show a => Show (Fml a) Source #	show instance
Instance details Defined in Data.Algorithm.SatSolver.Fml Methods showsPrec :: Int -> Fml a -> ShowS show :: Fml a -> String showList :: [Fml a] -> ShowS

constructing

mk :: Ord a => [Clause a] -> Fml a Source #

mk cs makes a forumula from a list of clauses. Duplicate clauses are removed.

>>> import qualified Data.Algoritm.SatSolver.Clause as Clause
>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> mk []
[]
>>> c1 = Clause.mk [Lit.mkPos' "x1", Lit.mkNeg' "x2", Lit.mkNeg' "x3"]
>>> c2 = Clause.mk [Lit.mkNeg' "x1", Lit.mkNeg' "x2"]
>>> c3 = Clause.mk [Lit.mkPos' "x1", Lit.mkPos' "x2", Lit.mkPos' "x3"]
>>> mk [c1, c2, c3]
[[-"x1",-"x2"],[+"x1",-"x2",-"x3"],[+"x1",+"x2",+"x3"]]

(/++/) :: Ord a => Fml a -> Fml a -> Fml a Source #

Union of two formulae.

>>> :type f
f :: Fml [Char]
>>> f
[[+"x1",-"x2",-"x3"],[-"x1",-"x2"],[+"x1",+"x2",+"x3"]]
>>> :type f'
f' :: Fml [Char]
>>> f'
[[+"x1"],[+"x3",-"x3"],[-"x1",+"x3"],[-"x2",+"x4"]]
f /++/ f'
[[+"x1",-"x2",-"x3"],[-"x1",-"x2"],[+"x1",+"x2",+"x3"],[+"x1"],[+"x3",-"x3"],[-"x1",+"x3"],[-"x2",+"x4"]]

testing

isEmpty :: Fml a -> Bool Source #

isEmpty f returns true if formula f contains no clause.

>>> let f = mk [] in isEmpty f
True

isSatisfied :: Fml a -> Bool Source #

isSatisfied f returns true if forumla f is satisfied. This reduces to testing if f contains no clause.

>>> let f = mk [] in isSatisfied f
True

hasUnsatisfiedClause :: Fml a -> Bool Source #

hasUnsatisfiedClause f returns true if formula f contains at least one empty clause.

>>> :type f
f :: Fml [Char]
>>> f
[[+"x1",-"x2",-"x3"],[],[-"x1",-"x2"],[+"x1",+"x2",+"x3"]]
>>> hasUnsatisfiedClause f
True
>>> :type f'
f' :: Fml [Char]
>>> f'
[[+"x1",-"x2",-"x3"],[-"x1",-"x2"],[+"x1",+"x2",+"x3"]]
>>> hasUnsatisfiedClause f'
False

querying

getLits :: Fml a -> [Lit a] Source #

getLits f returns all literals of formula f. Duplicate are not removed.

>>> let f = mk [] in getLits f
[]
>>> f
[[+"x1",-"x2",-"x3"],[-"x1",-"x2"],[+"x1",+"x2",+"x3"]]
>>> getLits f
[+"x1",-"x2",-"x3",-"x1",-"x2",+"x1",+"x2",+"x3"]

getVars :: Ord a => Fml a -> [Var a] Source #

getVars f returns the distinct propositional variables of formula f.

>>> let f = mk [] in getVars f
[]
>>> f
[[-"x1",-"x2"],[+"x1",-"x2",-"x3"],[+"x1",+"x2",+"x3"]]
>>> getVars f
["x1","x2","x3"]

getUnitClauses :: Ord a => Fml a -> [Clause a] Source #

getUnitClauses f returns the unit clauses of formula f.

>>> :type f
f :: Fml [Char]
>>> f
[[+"x1"],[-"x1",+"x2"],[-"x2"]]
>>> getUnitClauses f
[[+"x1"],[-"x2"]]

size :: Fml a -> Int Source #

size f returns the number of clauses (including empty clauses) in forumla f.

>>> :type f
f :: Fml [Char]
>>> f
[[-"x4",+"x5"],[+"x1",+"x3",-"x4"],[-"x1",+"x5"],[+"x1",+"x2"],[+"x1",-"x3"]]
>>> size f
5

selectMostFrequentLit :: Ord a => Fml a -> Maybe (Lit a) Source #

selectMostFrequentLit f returns the most frequent variable of formula f. The number of occurrences of a variable is the number of occurrences of the negative literals plus the number of occurrences of the positive literal.

>>> :type f
f :: Fml [Char]
>>> f
[[-"x4",+"x5"],[+"x1",+"x3",-"x4"],[-"x1",+"x5"],[+"x1",+"x2"],[+"x1",-"x3"]]
>>> Fml.selectMostFrequentLit f
Just +"x1"

selectMonotoneLit :: Ord a => Fml a -> Maybe (Lit a) Source #

selectMonotoneLit f returns (if any) a literal that occurs only negatively or only positively in formula f.

>>> selectMonotoneLit $ mk []
Nothing
>>> f
[[+1,+2],[-1,+3],[+1,+3],[-3,+4]]
>>> selectMonotoneLit f
Just +2
>>> f'
[[+1,+2],[-1,+3],[+1,+3],[-3,+4],[-2,-4]]
>>> selectMonotoneLit f'
Nothing

Transforming

toNormal :: (Ord a, Ord b, Num b, Enum b) => Fml a -> Fml b Source #

toNormal f transforms a CNF formula into normal form.

>>> :type f
f :: Fml [Char]
>>> f
[[-"x4",+"x5"],[+"x1",+"x3",-"x4"],[-"x1",+"x5"],[+"x1",+"x2"],[+"x1",-"x3"]]
>>> toNormal f
[[-4,+5],[+1,+3,-4],[-1,+5],[+1,+2],[+1,-3]]
>>> :type f'
f' :: Fml String
>>> f'
[[+"Evt A"],[-"Evt A",+"Evt B"],[-"Evt B",-"Evt C"],[-"Evt A",-"Evt B",+"Evt C"]]
>>> toNormal f'
[[+1],[-1,+2],[-2,-3],[-1,-2,+3]]

toDIMACSString :: Ord a => Fml a -> String Source #

toDIMACSString transforms CNF formula f into a DIMACS string.

>>> :type f
f :: Fml [Char]
>>> f
[[-"x4",+"x5"],[+"x1",+"x3",-"x4"],[-"x1",+"x5"],[+"x1",+"x2"],[+"x1",-"x3"]]
>>> putStr $ toDIMACSString f
c haskell rule
p cnf 9 9
+1 +2 0
+2 -3 0
-3 +4 0
+4 -5 0
-5 +6 0
+6 -7 0
-7 +8 0
+8 -9 0
-1 -9 0
>>> f'
[[+"Evt A",+"Evt B"],[-"Evt A",+"Evt C"],[+"Evt A",-"Evt B",-"Evt C"]]
>>> putStr $ toDIMACSString f'
c haskell rule
p cnf 3 3
+1 +2 0
-1 +3 0
+1 -2 -3 0