Portabilityportable
Stabilityprovisional
Safe HaskellNone

Dpfs.DavisPutnamFiniteSets

Contents

Description

Implementation of two extensions of the DPLL algorithm (Davis-Putnam-Logemann-Loveland)

First Extension:
Second Extension:

Synopsis

Datatype

data Atom

Constructors

Xin !Int !IntSet 
Calc !IntSet !IntSet 

Instances

Eq Atom 
Show Atom 

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

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

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

setToInt :: Int -> SolutionSet -> Int

dpcnf :: FiniteSet -> Pexpr (Int, [Int]) -> KlauselMenge

expectJust :: Maybe a -> a

toList' :: IntSet -> [Int]