atp-haskell-1.8: Translation from Ocaml to Haskell of John Harrison's ATP code

Safe HaskellNone
LanguageHaskell98

Data.Logic.ATP.DP

Description

The Davis-Putnam and Davis-Putnam-Loveland-Logemann procedures.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Synopsis

Documentation

dp :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool Source

The DP procedure.

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.

dplisat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool Source

dplitaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool Source

dpll :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool Source

The same thing but with the DPLL procedure. (p. 84)

dpllsat :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool Source

dplltaut :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool Source

dplb :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool Source

With simple non-chronological backjumping and learning.

dplbsat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool Source

dplbtaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool Source

testDP :: Test Source