| Copyright | (c) Stéphane Vialette, 2014 |
|---|---|
| License | MIT |
| Maintainer | vialette@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
SatSolver
Description
- selectLiteral :: Formula -> Literal
- reduceFormula :: Literal -> Formula -> Formula
- reduceClause :: Literal -> Clause -> Clause
- solve :: Formula -> Maybe (Map Variable Bool)
Documentation
selectLiteral :: Formula -> Literal
The selectLiteral function return a literal in the clause.
If the clause contains contains at least one unit clause, the
function returns a literal in a unit clause.
Otherwise it returns a literal that occurs the most frequently.
>>>selectLiteral $ F.makeFormula [[1,2], [3], [1,2], [4]]3>>>selectLiteral $ F.makeFormula [[1,2], [3,4], [1,3]]3
This function should not be part of the public interface of the module.
reduceFormula :: Literal -> Formula -> Formula
The reduceFormula function reduce 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.
reduceClause :: Literal -> Clause -> Clause
The reduceClause function reduces a clause according to a given literal:
it removes the opposite occurrence (if any) of the literal.
>>>reduceClause 1 $ C.makeClause [][]>>>reduceClause 1 $ C.makeClause [1, 2, 3][1,2,3]>>>reduceClause 1 $ C.makeClause [-1, 2, 3][2,3]
This function should not be part of the public interface of the module.
solve :: Formula -> Maybe (Map Variable Bool)
The solve function returns Nothing if the formula is not satisfiable.
Ohherwise it returns a satisfying assignment (possibly incomplete) in the
form of a map.
>>>solve $ F.makeFormula [[1,2], [-1,-2], [2,3], [1,-2], [-2,4]]Just (fromList [(1,True),(2,False),(3,True)])>>>solve $ F.makeFormula [[1,2], [-1,2], [1,-2], [-1,-2]]Nothing
This function should not be part of the public interface of the module.