DavisPutnamFiniteSets

Synopsis

Documentation

data Atom

Constructors

Xin (Int, IntSet)

Xin constructor for representing an 2-tupel for variables as Int and the finite set.

Instances

Eq Atom 
Show Atom 

type Klausel = [Atom]

type AtomTupel = (Int, IntSet)

type FiniteSet = Int

dpfs :: KlauselMenge -> FiniteSet -> Klausel

dpfs function describes the procedure of the Davis-Putnam algorithm.

findTrueFalse :: FiniteSet -> KlauselMenge -> Maybe Atom

Problem Literal in clause set

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

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.

isXinAtom :: Atom -> Bool

showLiteral :: Atom -> Int

showSet :: Atom -> IntSet

showXin :: [Atom] -> Int

atomToTupel :: Atom -> (Int, IntSet)

The helper atomToTupel returns an tupel from the Xin data constructor.

elem' :: Int -> [Atom] -> Bool

The helper elem' indicates if the atom member of one given clause.

elem1 :: Int -> Klausel -> [Atom]

The helper elem' indicates if the atom member of one given clause. elem1 :: Int -> [Atom] -> Bool

elem'' :: (Int, IntSet) -> [Atom] -> Bool

The helper elem' indicates if the atom member of one given clause.

lookup' :: Int -> [Atom] -> Maybe IntSet

The helper lookup' function looks up a set of one literal a

setToInt :: Int -> Klausel -> Int