| Copyright | (c) Stéphane Vialette, 2014 |
|---|---|
| License | MIT |
| Maintainer | vialette@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
SatSolver
Description
Documentation
selectLiteral :: (Eq a, Ord a) => Formula a -> Literal a
solve :: Ord a => Formula a -> Maybe (Map (Variable a) 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