| Copyright | (c) Stéphane Vialette, 2014 |
|---|---|
| License | MIT |
| Maintainer | vialette@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
Formula
Description
Here is a longer description of this module, containing some
commentary with some markup.
- type Formula = [Clause]
- makeFormula :: [Clause] -> Formula
- isEmpty :: Formula -> Bool
- isSatisfied :: Formula -> Bool
- unitClauses :: Formula -> Formula
- mostFrequentLiteral :: Formula -> Literal
- hasUnsatisfiedClause :: Formula -> Bool
- makeExampleFormula :: Formula
Documentation
makeFormula :: [Clause] -> Formula
The makeFormula function constructs a formula from a list of clauses.
Duplicate clauses are removed.
>>>makeFormula [][]>>>makeFormula [[1], [2,3]][[1],[2,3]]>>>makeFormula [[1], [2,3], [3,2], [1]][[1],[2,3]]
The isEmpty function return True if the formula is empty.
>>>isEmpty $ makeFormula []True>>>isEmpty $ makeFormula [[1,2], [3]]False
isSatisfied :: Formula -> Bool
The isSatisfied function return True if the formula is empty.
(See isEmpty.)
unitClauses :: Formula -> Formula
The unitClauses function takes a formula and returns a new formula
made of those unit clauses.
>>>unitClauses $ makeFormula [[1], [-2,3], [4], [5,6,7]][[1],[4]]
mostFrequentLiteral :: Formula -> Literal
The mostFrequentLiteral function takes a formula and returns one
literal that occurs more frequently.
>>>mostFrequentLiteral $ makeFormula [[1], [-1,-2], [1,2,-3], [2,3]]2
hasUnsatisfiedClause :: Formula -> Bool
The hasUnsatisfiedClause function takes a formula and returns True if it
contains at least one empty clause.
The makeExampleFormula returns an example formula using both
makeClause and makeFormula.
>>>makeExampleFormula[[-3,1],[-5,1,4],[2,3,4],[-5,-3,-1],[4,5],[-4,-3,5],[2],[-2,1]]