DavisPutnamFiniteSets
- data Atom = Xin (Int, IntSet)
- type Klausel = [Atom]
- type KlauselMenge = [Klausel]
- type AtomTupel = (Int, IntSet)
- type FiniteSet = Int
- dpfs :: KlauselMenge -> FiniteSet -> Klausel
- dpfsAlle :: KlauselMenge -> FiniteSet -> KlauselMenge
- dpfsSat :: KlauselMenge -> FiniteSet -> Klausel -> Klausel
- dpfsSatAlle :: KlauselMenge -> FiniteSet -> KlauselMenge -> KlauselMenge
- findTrueFalse :: FiniteSet -> KlauselMenge -> Maybe Atom
- resolveTrueFalse :: Int -> AtomTupel -> KlauselMenge -> KlauselMenge
- resolveTrueFalse' :: Int -> AtomTupel -> [Atom] -> KlauselMenge -> KlauselMenge
- findUnit :: KlauselMenge -> Maybe Atom
- findUnit' :: KlauselMenge -> Maybe AtomTupel
- isRemoveable :: (Int, IntSet) -> Klausel -> Bool
- findSimilarAtomUnits :: Int -> KlauselMenge -> Maybe Atom
- resolveSimilarAtomUnits' :: Int -> Klausel -> IntSet
- resolveSimilarAtomUnits :: Klausel -> Klausel -> Atom
- substituteSimilarUnits :: AtomTupel -> KlauselMenge -> KlauselMenge
- findPureLiteral :: KlauselMenge -> Maybe AtomTupel
- resolvePureLiteral :: AtomTupel -> KlauselMenge -> KlauselMenge
- countElems :: [(Key, IntSet)] -> (Int, IntSet)
- countElems2 :: [(Key, IntSet)] -> (Int, IntSet)
- findBestLiteral :: KlauselMenge -> (Int, IntSet)
- isXinAtom :: Atom -> Bool
- showLiteral :: Atom -> Int
- showSet :: Atom -> IntSet
- showXin :: [Atom] -> Int
- atomToTupel :: Atom -> (Int, IntSet)
- elem' :: Int -> [Atom] -> Bool
- elem1 :: Int -> Klausel -> [Atom]
- elem'' :: (Int, IntSet) -> [Atom] -> Bool
- lookup' :: Int -> [Atom] -> Maybe IntSet
- setToInt :: Int -> Klausel -> Int
Documentation
data Atom
type KlauselMenge = [Klausel]
type AtomTupel = (Int, IntSet)
type FiniteSet = Int
dpfs :: KlauselMenge -> FiniteSet -> Klausel
dpfs
function describes the procedure of the Davis-Putnam algorithm.
dpfsAlle :: KlauselMenge -> FiniteSet -> KlauselMenge
dpfsSat :: KlauselMenge -> FiniteSet -> Klausel -> Klausel
dpfsSatAlle :: KlauselMenge -> FiniteSet -> KlauselMenge -> KlauselMenge
findTrueFalse :: FiniteSet -> KlauselMenge -> Maybe Atom
Problem Literal in clause set
resolveTrueFalse :: Int -> AtomTupel -> KlauselMenge -> KlauselMenge
resolveTrueFalse' :: Int -> AtomTupel -> [Atom] -> KlauselMenge -> KlauselMenge
findUnit :: KlauselMenge -> Maybe Atom
The findUnit
function return the first unit from the clause set if one exist.
findUnit' :: KlauselMenge -> Maybe AtomTupel
The findUnit'
function return the first unit (a elem M') from the clause set if one exist.
isRemoveable :: (Int, IntSet) -> Klausel -> Bool
The removeable
function indicates whenever an given clause could be removed from the clause set.
findSimilarAtomUnits :: Int -> KlauselMenge -> Maybe Atom
The findSimilarAtomUnits
function interates through the clause set and returns the first unit a.
resolveSimilarAtomUnits' :: Int -> Klausel -> IntSet
resolveSimilarAtomUnits :: Klausel -> Klausel -> Atom
substituteSimilarUnits :: AtomTupel -> KlauselMenge -> KlauselMenge
The substituteSimilarUnits
function return an clause set where subsum all occurrences of one unit to one unit.
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.
countElems :: [(Key, IntSet)] -> (Int, IntSet)
countElems2 :: [(Key, IntSet)] -> (Int, IntSet)
findBestLiteral :: KlauselMenge -> (Int, IntSet)
The findBestLiteral
function returns an literal of the given claus set where the literal occours at most in any clauses and the finite set is possibly small.
showLiteral :: Atom -> Int
atomToTupel :: Atom -> (Int, IntSet)
The helper atomToTupel
returns an tupel from the Xin data constructor.
elem1 :: Int -> Klausel -> [Atom]
The helper elem'
indicates if the atom member of one given clause.
elem1 :: Int -> [Atom] -> Bool