| License | GNU LGPLv3 |
|---|---|
| Maintainer | paul.bittner@uni-ulm.de |
| Safe Haskell | None |
SAT
Description
Module for sat solving on PropositionalFormulas.
Uses the picosat library.
Synopsis
- sat :: (Show a, Ord a) => PropositionalFormula a -> Bool
- satAssignment :: (Show a, Ord a) => PropositionalFormula a -> Maybe (Assignment a)
- tautCounterExample :: (Show a, Ord a) => PropositionalFormula a -> Maybe (Assignment a)
- taut :: (Show a, Ord a) => PropositionalFormula a -> Bool
- contradicts :: (Show a, Ord a) => PropositionalFormula a -> Bool
- toIntCNF :: Ord a => PropositionalFormula a -> ([[Int]], Bimap a Int)
Documentation
sat :: (Show a, Ord a) => PropositionalFormula a -> Bool Source #
Returns true iff the given propositional formula is satisfiable.
satAssignment :: (Show a, Ord a) => PropositionalFormula a -> Maybe (Assignment a) Source #
Returns a satisfying assignment Just a for the given propositional formula
iff the formula is satisfiable.
Returns Nothing otherwise.
tautCounterExample :: (Show a, Ord a) => PropositionalFormula a -> Maybe (Assignment a) Source #
Returns Nothing iff the given formula is a tautology.
Otherwise, returns a counterexample (i.e., an assignment under which the given formula evaluates to false).
taut :: (Show a, Ord a) => PropositionalFormula a -> Bool Source #
Returns true iff the given propositional formula is a tautology.
contradicts :: (Show a, Ord a) => PropositionalFormula a -> Bool Source #
Returns true iff the given formula is not satisfiable (i.e., there is no assignment making it true).
toIntCNF :: Ord a => PropositionalFormula a -> ([[Int]], Bimap a Int) Source #
Converts the given formula to a list of clauses (first argument).
Each clause is represented as a list of literals where literals are represented as integers.
Negative literals indicate negation of variables.
For example, the literal -3 translates to PNot x, where x is the variable represented by 3.
The mapping from integers to variables is returned as a bimap in the second argument.