Safe Haskell | Safe |
---|
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
Fml
type
Fml | |
|
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
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