Portability | portable |
---|---|
Stability | provisional |
Safe Haskell | None |
Dpfs.DavisPutnamFiniteSets
Description
Implementation of two extensions of the DPLL algorithm (Davis-Putnam-Logemann-Loveland)
First Extension:
Second Extension:
- data Atom
- dpfs :: FiniteSet -> [Char] -> [Char]
- dpfsAll :: Int -> [Char] -> [[(String, IntSet)]]
- dpfsSat :: CalculusSwitch -> FiniteSet -> KlauselMenge -> SolutionSet
- dpfsSatAllSolutions :: CalculusSwitch -> FiniteSet -> KlauselMenge -> KlauselMenge
- findTrueFalse :: Int -> KlauselMenge -> Maybe Atom
- resolveTrueFalse :: Int -> Atom -> KlauselMenge -> KlauselMenge
- findSimilarAtomUnits :: Int -> KlauselMenge -> Maybe Atom
- substituteSimilarUnits :: Atom -> KlauselMenge -> KlauselMenge
- findUnit' :: KlauselMenge -> Maybe AtomTupel
- resolveUnit :: AtomTupel -> KlauselMenge -> KlauselMenge
- findPureLiteral :: KlauselMenge -> Maybe AtomTupel
- resolvePureLiteral :: AtomTupel -> KlauselMenge -> KlauselMenge
- findUnit' :: KlauselMenge -> Maybe AtomTupel
- resolveUnitCalculus :: AtomTupel -> KlauselMenge -> KlauselMenge
- findSimpRule3 :: KlauselMenge -> SolutionSet -> Maybe ((Int, IntSet), Atom)
- resolveSimpRule3 :: ((Int, IntSet), Atom) -> KlauselMenge -> SolutionSet -> SolutionSet
- findFalse_Calculus :: KlauselMenge -> Maybe Atom
- resolveFalse_Calculus :: KlauselMenge -> KlauselMenge
- findSimpUnitCalculus :: KlauselMenge -> SolutionSet -> Maybe (Atom, SolutionSet)
- resolveCalculus1 :: Atom -> KlauselMenge -> SolutionSet -> KlauselMenge
- findSelection2 :: KlauselMenge -> SolutionSet -> Maybe Atom
- setSplit2 :: Atom -> KlauselMenge -> SolutionSet -> KlauselMenge
- lookup' :: Int -> [Atom] -> Maybe IntSet
- setToInt :: Int -> SolutionSet -> Int
- dpcnf :: FiniteSet -> Pexpr (Int, [Int]) -> KlauselMenge
- expectJust :: Maybe a -> a
- toList' :: IntSet -> [Int]
Datatype
Davis-Putnam procedures
dpfs :: FiniteSet -> [Char] -> [Char]
dpfs
function executes the following parts:
- parsing the formula
- cnf transformation
- dp procedure extension 1
dpfsAll :: Int -> [Char] -> [[(String, IntSet)]]
dpfsAll
function executes the following parts:
- parsing the formula
- cnf transformation
- dp procedure extension 1 and tries to find all solutions
dpfsSat :: CalculusSwitch -> FiniteSet -> KlauselMenge -> SolutionSet
dpfsSat
function describes the procedure of the Davis-Putnam algorithm and returns one solutions if one exists.
dpfsSatAllSolutions :: CalculusSwitch -> FiniteSet -> KlauselMenge -> KlauselMenge
dpfsAllSolutions
function describes the procedure of the Davis-Putnam algorithm and returns all solutions if any exists.
Rules: 1st Extension
findTrueFalse :: Int -> KlauselMenge -> Maybe Atom
findTrueFalse
runs through the clause set and returns an atom which can be simplify.
resolveTrueFalse :: Int -> Atom -> KlauselMenge -> KlauselMenge
resolveTrueFalse
simplfies the clause set for the given atom.
findSimilarAtomUnits :: Int -> KlauselMenge -> Maybe Atom
The findSimilarAtomUnits
function interates through the clause set and returns the first unit a.
substituteSimilarUnits :: Atom -> KlauselMenge -> KlauselMenge
findUnit' :: KlauselMenge -> Maybe AtomTupel
The findUnit'
function return the first unit (a elem M') from the clause set if one exist.
resolveUnit :: AtomTupel -> KlauselMenge -> KlauselMenge
findPureLiteral :: KlauselMenge -> Maybe AtomTupel
The findPureLiteral
function returns the first pure literal.
resolvePureLiteral :: AtomTupel -> KlauselMenge -> KlauselMenge
The resolvePureLiteral
builds up a new clause set while skipping clauses which contains the pure unit.
Rules: 2nd Extension
findUnit' :: KlauselMenge -> Maybe AtomTupel
The findUnit'
function return the first unit (a elem M') from the clause set if one exist.
resolveUnitCalculus :: AtomTupel -> KlauselMenge -> KlauselMenge
The resolveUnitCalculus
function removes the given atom from the clause set.
findSimpRule3 :: KlauselMenge -> SolutionSet -> Maybe ((Int, IntSet), Atom)
The findSimpRule3
function runs through the clause set and returns an Atom if any simplifications are possible for rule 3.
resolveSimpRule3 :: ((Int, IntSet), Atom) -> KlauselMenge -> SolutionSet -> SolutionSet
The resolveSimpRule3
function updates the solutionSet for the given calc atom
findFalse_Calculus :: KlauselMenge -> Maybe Atom
The findFalse_Calculus
find the first calc atom with one or both sets are empty.
resolveFalse_Calculus :: KlauselMenge -> KlauselMenge
The resolveFalse_Calculus
function runs through the clause set and removes all atoms with one or both sets are empty.
findSimpUnitCalculus :: KlauselMenge -> SolutionSet -> Maybe (Atom, SolutionSet)
The findSimpUnitCalculus
function runs through the clause set and returns an Atom if any simplifications are possible. (Rule 1 + 2)
resolveCalculus1 :: Atom -> KlauselMenge -> SolutionSet -> KlauselMenge
The resolveCalculus
function simplifies the clause set an returns the updated clause set (Rule 1 + 2)
findSelection2 :: KlauselMenge -> SolutionSet -> Maybe Atom
The findSelection
function returns an calc atom, if and only if this calc atom is splitable into two pieces.
setSplit2 :: Atom -> KlauselMenge -> SolutionSet -> KlauselMenge
The setSplit
function splits the passed calc atom into two ore more pieces.
Utilities
setToInt :: Int -> SolutionSet -> Int
expectJust :: Maybe a -> a