| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Logic.ATP.DP
Contents
Description
The Davis-Putnam and Davis-Putnam-Loveland-Logemann procedures.
Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
Synopsis
- 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)
dplb :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool Source #
With simple non-chronological backjumping and learning.