Safe Haskell | None |
---|---|
Language | Haskell98 |
The Davis-Putnam and Davis-Putnam-Loveland-Logemann procedures.
Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
- dp :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
- dpsat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
- dptaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
- dpli :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool
- dplisat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
- dplitaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
- dpll :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
- dpllsat :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool
- dplltaut :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool
- dplb :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool
- dplbsat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
- dplbtaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
- testDP :: Test
Documentation
dpsat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool Source
Davis-Putnam satisfiability tester.
dptaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool Source
Davis-Putnam tautology checker.
dpli :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool Source
Iterative implementation with explicit trail instead of recursion.
dpll :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool Source
The same thing but with the DPLL procedure. (p. 84)