Copyright	(c) Stéphane Vialette, 2015
License	MIT
Maintainer	vialette@gmail.com
Stability	experimental
Safe Haskell	Safe-Inferred

Formula

Description

Synopsis

Documentation

data Formula a

Formula type

Constructors

Formula [Clause a]

Instances

Show a => Show (Formula a)

makeFormula :: Ord a => [[Literal a]] -> Formula a

The makeFormula function constructs a formula from a list of lists of literals. Duplicate clauses and tautologies are removed.

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n1 = L.Negative (V.Variable "x1")
>>> let p2 = L.Positive (V.Variable "x2")
>>> let n2 = L.Negative (V.Variable "x2")
>>> let p3 = L.Positive (V.Variable "x3")
>>> let n3 = L.Negative (V.Variable "x3")
>>> makeFormula [[p1],[p1,n2],[n2,p3,n3],[p1,n2,p3,n2],[p1,n2]]
Formula [Clause [Positive (Variable "x1")],
         Clause [Negative (Variable "x2"),Positive (Variable "x1")],
         Clause [Negative (Variable "x2"),Positive (Variable "x1"),Positive (Variable "x3")]]
>>>

makeFormula_ :: Ord a => [Clause a] -> Formula a

The makeFormula_ function constructs a formula from a list of clauses. Duplicate clauses and tautologies are removed.

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n1 = L.Negative (V.Variable "x1")
>>> let p2 = L.Positive (V.Variable "x2")
>>> let n2 = L.Negative (V.Variable "x2")
>>> let p3 = L.Positive (V.Variable "x3")
>>> let n3 = L.Negative (V.Variable "x3")
>>> makeFormula_ $ List.map C.makeClause [[p1],[p1,n2],[n2,p3,n3],[p1,n2,p3,n2],[p1,n2]]
Formula [Clause [Positive (Variable "x1")],
         Clause [Negative (Variable "x2"),Positive (Variable "x1")],
         Clause [Negative (Variable "x2"),Positive (Variable "x1"),Positive (Variable "x3")]]

reduce :: (Eq a, Ord a) => Formula a -> Literal a -> Formula a

The reduce function reduces a formula according to a literal. Occurrences of the opposite literal are removed and clauses containing this literal are removed.

>>> reduceFormula 1 $ F.makeFormula [[1,2],[-1,-2],[2,3],[1,-2]]
[[-2],[2,3]]

This function should not be part of the public interface of the module.

isSatisfied :: Formula a -> Bool

The isSatisfied function return True if the formula is empty.

hasUnsatisfiedClause :: Formula a -> Bool

The hasUnsatisfiedClause function takes a formula and returns True if it contains at least one empty clause.

unitClauses :: Formula a -> [Clause a]

The unitClauses function takes a formula and returns a the list of all unit clauses.

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n1 = L.Negative (V.Variable "x1")
>>> let p2 = L.Positive (V.Variable "x2")
>>> let n2 = L.Negative (V.Variable "x2")
>>> let p3 = L.Positive (V.Variable "x3")
>>> let n3 = L.Negative (V.Variable "x3")
>>> unitClauses $ makeFormula [[1], [-2,3], [4], [5,6,7]]
[[1],[4]]

mostFrequentLiteral :: (Eq a, Ord a) => Formula a -> Literal a

The mostFrequentLiteral function takes a formula and returns a literal that occurs more frequently.

>>> mostFrequentLiteral $ makeFormula [[1], [-1,-2], [1,2,-3], [2,3]]
2

example :: Formula [Char]

The example returns an example formula using both makeClause and 'makeFormula_.

>>> example
Formula [Clause [Positive (Variable "x1"),Positive (Variable "x1"),Negative (Variable "x2")],
         Clause [Positive (Variable "x1"),Negative (Variable "x3"),Positive (Variable "x7")],
         Clause [Positive (Variable "x1"),Positive (Variable "x2"),Negative (Variable "x3")],
         Clause [Negative (Variable "x1"),Negative (Variable "x2"),Negative (Variable "x4")],
         Clause [Negative (Variable "x2"),Positive (Variable "x3"),Positive (Variable "x5")],
         Clause [Negative (Variable "x6")],
         Clause [Negative (Variable "x3"),Negative (Variable "x5"),Positive (Variable "x6")],
         Clause [Negative (Variable "x4"),Positive (Variable "x6"),Positive (Variable "x7")]]