diff --git a/Data/Boolean.hs b/Data/Boolean.hs
new file mode 100644
--- /dev/null
+++ b/Data/Boolean.hs
@@ -0,0 +1,157 @@
+{-# OPTIONS -fno-warn-incomplete-patterns #-}
+-- |
+-- Module      : Data.Boolean
+-- Copyright   : Sebastian Fischer
+-- License     : BSD3
+-- 
+-- Maintainer  : Sebastian Fischer (sebf@informatik.uni-kiel.de)
+-- Stability   : experimental
+-- Portability : portable
+-- 
+-- This library provides a representation of boolean formulas that is
+-- used by the solver in "Data.Boolean.SatSolver".
+-- 
+-- We also define a function to simplify formulas, a type for
+-- conjunctive normalforms, and a function that creates them from
+-- boolean formulas.
+-- 
+module Data.Boolean ( 
+
+  Boolean(..), 
+
+  Literal(..), literalVar, invLiteral, isPositiveLiteral, 
+
+  CNF, Clause, booleanToCNF
+
+  ) where
+
+import Data.Maybe ( mapMaybe )
+import qualified Data.IntMap as IM
+
+import Control.Monad ( guard, liftM )
+
+-- | Boolean formulas are represented as values of type @Boolean@.
+-- 
+data Boolean
+  -- | Variables are labeled with an @Int@,
+  = Var Int
+  -- | @Yes@ represents /true/,
+  | Yes
+  -- | @No@ represents /false/,
+  | No
+  -- | @Not@ constructs negated formulas,
+  | Not Boolean
+  -- | and finally we provide conjunction
+  | Boolean :&&: Boolean
+  -- | and disjunction of boolean formulas.
+  | Boolean :||: Boolean
+ deriving Show
+
+-- | Literals are variables that occur either positively or negatively.
+-- 
+data Literal = Pos Int | Neg Int deriving (Eq, Show)
+
+-- | This function returns the name of the variable in a literal.
+-- 
+literalVar :: Literal -> Int
+literalVar (Pos n) = n
+literalVar (Neg n) = n
+
+-- | This function negates a literal.
+-- 
+invLiteral :: Literal -> Literal
+invLiteral (Pos n) = Neg n
+invLiteral (Neg n) = Pos n
+
+-- | This predicate checks whether the given literal is positive.
+-- 
+isPositiveLiteral :: Literal -> Bool
+isPositiveLiteral (Pos _) = True
+isPositiveLiteral _       = False
+
+-- | Conjunctive normalforms are lists of lists of literals.
+-- 
+type CNF     = [Clause]
+type Clause  = [Literal]
+
+-- | 
+-- We convert boolean formulas to conjunctive normal form by pushing
+-- negations down to variables and repeatedly applying the
+-- distributive laws.
+-- 
+booleanToCNF :: Boolean -> CNF
+booleanToCNF
+  = mapMaybe (simpleClause . map literal . disjunction)
+  . conjunction
+  . asLongAsPossible distribute
+  . asLongAsPossible pushNots
+  . asLongAsPossible elim
+ where
+  elim (Not Yes)      = Just No
+  elim (Not No)       = Just Yes
+  elim (No  :&&: _)   = Just No
+  elim (Yes :&&: x)   = Just x
+  elim (_   :&&: No)  = Just No
+  elim (x   :&&: Yes) = Just x 
+  elim (Yes :||: _)   = Just Yes
+  elim (No  :||: x)   = Just x
+  elim (_   :||: Yes) = Just Yes
+  elim (x   :||: No)  = Just x
+  elim _              = Nothing
+
+  pushNots (Not (Not x))  = Just x
+  pushNots (Not (x:&&:y)) = Just (Not x :||: Not y)
+  pushNots (Not (x:||:y)) = Just (Not x :&&: Not y)
+  pushNots _              = Nothing
+
+  distribute (x:||:(y:&&:z)) = Just ((x:||:y):&&:(x:||:z))
+  distribute ((x:&&:y):||:z) = Just ((x:||:z):&&:(y:||:z))
+  distribute _               = Nothing
+
+  literal (Var x)       = Pos x
+  literal (Not (Var x)) = Neg x
+
+
+-- private helper functions
+
+-- remove duplicate literals from clauses and drop clauses that
+-- contain one literal both positively and negatively.
+--
+simpleClause :: Clause -> Maybe Clause
+simpleClause = liftM (map lit . IM.toList) . foldl add (Just IM.empty)
+ where
+  lit (x,True)  = Pos x
+  lit (x,False) = Neg x
+
+  add mm l = do
+    m <- mm
+    let x = literalVar l; kind = isPositiveLiteral l
+    maybe (Just (IM.insert x kind m))
+          (\b -> guard (b==kind) >> Just m)
+          (IM.lookup x m)
+
+conjunction :: Boolean -> [Boolean]
+conjunction b = flat b []
+ where flat Yes      = id
+       flat (x:&&:y) = flat x . flat y
+       flat x        = (x:)
+
+disjunction :: Boolean -> [Boolean]
+disjunction b = flat b []
+ where flat No       = id
+       flat (x:||:y) = flat x . flat y
+       flat x        = (x:)
+
+asLongAsPossible :: (Boolean -> Maybe Boolean) -> Boolean -> Boolean
+asLongAsPossible f = everywhere g
+ where g x = maybe x (everywhere g) (f x)
+
+everywhere :: (Boolean -> Boolean) -> Boolean -> Boolean
+everywhere f = f . atChildren (everywhere f)
+
+atChildren :: (Boolean -> Boolean) -> Boolean -> Boolean
+atChildren f (Not x)  = Not (f x)
+atChildren f (x:&&:y) = f x :&&: f y
+atChildren f (x:||:y) = f x :||: f y
+atChildren _ x        = x
+
diff --git a/Data/Boolean/SatSolver.hs b/Data/Boolean/SatSolver.hs
new file mode 100644
--- /dev/null
+++ b/Data/Boolean/SatSolver.hs
@@ -0,0 +1,183 @@
+-- |
+-- Module      : Data.Boolean.SatSolver
+-- Copyright   : Sebastian Fischer
+-- License     : BSD3
+-- 
+-- Maintainer  : Sebastian Fischer (sebf@informatik.uni-kiel.de)
+-- Stability   : experimental
+-- Portability : portable
+-- 
+-- This Haskell library provides an implementation of the
+-- Davis-Putnam-Logemann-Loveland algorithm
+-- (cf. <http://en.wikipedia.org/wiki/DPLL_algorithm>) for the boolean
+-- satisfiability problem. It not only allows to solve boolean
+-- formulas in one go but also to add constraints and query bindings
+-- of variables incrementally.
+-- 
+-- The implementation is not sophisticated at all but uses the basic
+-- DPLL algorithm with unit propagation.
+-- 
+module Data.Boolean.SatSolver (
+
+  Boolean(..), SatSolver, Literal(..), literalVar, invLiteral, isPositiveLiteral, CNF, Clause, booleanToCNF,
+
+  newSatSolver, isSolved, 
+
+  lookupVar, assertTrue, assertTrue', branchOnVar, selectBranchVar, solve, isSolvable
+
+  ) where
+
+import Data.List
+import Data.Boolean
+
+import Control.Monad.Writer
+
+import qualified Data.IntMap as IM
+
+-- | A @SatSolver@ can be used to solve boolean formulas.
+-- 
+data SatSolver = SatSolver { clauses :: CNF, bindings :: IM.IntMap Bool }
+ deriving Show
+
+-- | A new SAT solver without stored constraints.
+-- 
+newSatSolver :: SatSolver
+newSatSolver = SatSolver [] IM.empty
+
+-- | This predicate tells whether all constraints are solved.
+-- 
+isSolved :: SatSolver -> Bool
+isSolved = null . clauses
+
+-- |
+-- We can lookup the binding of a variable according to the currently
+-- stored constraints. If the variable is unbound, the result is
+-- @Nothing@.
+-- 
+lookupVar :: Int -> SatSolver -> Maybe Bool
+lookupVar name = IM.lookup name . bindings
+
+-- | 
+-- We can assert boolean formulas to update a @SatSolver@. The
+-- assertion may fail if the resulting constraints are unsatisfiable.
+-- 
+assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver
+assertTrue formula solver = do
+  newClauses <- foldl (addClause (bindings solver))
+                      (return (clauses solver))
+                      (booleanToCNF formula)
+  simplify (solver { clauses = newClauses })
+
+assertTrue' :: MonadPlus m => CNF -> SatSolver -> m SatSolver
+assertTrue' formula solver = do
+  newClauses <- foldl (addClause (bindings solver))
+                      (return (clauses solver))
+                      formula
+  simplify (solver { clauses = newClauses })
+
+-- |
+-- This function guesses a value for the given variable, if it is
+-- currently unbound. As this is a non-deterministic operation, the
+-- resulting solvers are returned in an instance of @MonadPlus@.
+-- 
+branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolver
+branchOnVar name solver =
+  maybe (branchOnUnbound name solver)
+        (const (return solver))
+        (lookupVar name solver)
+
+-- |
+-- We select a variable from the shortest clause hoping to produce a
+-- unit clause.
+--
+selectBranchVar :: SatSolver -> Int
+selectBranchVar = literalVar . head . head . sortBy shorter . clauses
+
+-- | 
+-- This function guesses values for variables such that the stored
+-- constraints are satisfied. The result may be non-deterministic and
+-- is, hence, returned in an instance of @MonadPlus@.
+-- 
+solve :: MonadPlus m => SatSolver -> m SatSolver
+solve solver
+  | isSolved solver = return solver
+  | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= solve
+
+-- |
+-- This predicate tells whether the stored constraints are
+-- solvable. Use with care! This might be an inefficient operation. It
+-- tries to find a solution using backtracking and returns @True@ if
+-- and only if that fails.
+-- 
+isSolvable :: SatSolver -> Bool
+isSolvable = not . null . solve
+
+
+-- private helper functions
+
+addClause :: MonadPlus m => IM.IntMap Bool -> m [Clause] -> Clause -> m [Clause]
+addClause binds mclauses newClause = do
+  oldClauses <- mclauses
+  let unboundLits = foldl (addUnbound binds) (Just []) newClause
+  maybe (return oldClauses)
+        (\lits -> guard (not (null lits)) >> return (lits:oldClauses))
+        unboundLits
+
+addUnbound :: IM.IntMap Bool -> Maybe Clause -> Literal -> Maybe Clause
+addUnbound binds mlits lit = do
+  lits <- mlits
+  maybe (Just (lit:lits))
+        (\b -> guard (b /= isPositiveLiteral lit) >> return lits)
+        (IM.lookup (literalVar lit) binds)
+
+updateSolver :: MonadPlus m => CNF -> [(Int,Bool)] -> SatSolver -> m SatSolver
+updateSolver cs bs solver = do
+  bs' <- foldr (uncurry insertBinding) (return (bindings solver)) bs
+  return $ solver { clauses = cs, bindings = bs' }
+
+insertBinding :: MonadPlus m
+              => Int -> Bool -> m (IM.IntMap Bool) -> m (IM.IntMap Bool)
+insertBinding name newValue binds = do
+  bs <- binds
+  maybe (return (IM.insert name newValue bs))
+        (\oldValue -> do guard (oldValue==newValue); return bs)
+        (IM.lookup name bs)
+
+simplify :: MonadPlus m => SatSolver -> m SatSolver
+simplify solver = do
+  (cs,bs) <- runWriterT . simplifyClauses . clauses $ solver
+  updateSolver cs bs solver
+
+simplifyClauses :: MonadPlus m => CNF -> WriterT [(Int,Bool)] m CNF
+simplifyClauses [] = return []
+simplifyClauses allClauses = do
+  let shortestClause = head . sortBy shorter $ allClauses
+  guard (not (null shortestClause))
+  if null (tail shortestClause)
+   then propagate (head shortestClause) allClauses >>= simplifyClauses
+   else return allClauses
+
+propagate :: MonadPlus m => Literal -> CNF -> WriterT [(Int,Bool)] m CNF
+propagate literal allClauses = do
+  tell [(literalVar literal, isPositiveLiteral literal)]
+  return (foldr prop [] allClauses)
+ where
+  prop c cs | literal `elem` c = cs
+            | otherwise        = filter (invLiteral literal/=) c : cs
+
+branchOnUnbound :: MonadPlus m => Int -> SatSolver -> m SatSolver
+branchOnUnbound name solver =
+  guess (Pos name) solver `mplus` guess (Neg name) solver
+
+guess :: MonadPlus m => Literal -> SatSolver -> m SatSolver
+guess literal solver = do
+  (cs,bs) <- runWriterT (propagate literal (clauses solver) >>= simplifyClauses)
+  updateSolver cs bs solver
+
+shorter :: [a] -> [a] -> Ordering
+shorter []     []     = EQ
+shorter []     _      = LT
+shorter _      []     = GT
+shorter (_:xs) (_:ys) = shorter xs ys
+
+
diff --git a/Data/Logic/Classes/Literal.hs b/Data/Logic/Classes/Literal.hs
--- a/Data/Logic/Classes/Literal.hs
+++ b/Data/Logic/Classes/Literal.hs
@@ -10,7 +10,6 @@
     , foldAtomsLiteral
     ) where
 
-import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Combine (Combination(..))
 import Data.Logic.Classes.Constants
 import qualified Data.Logic.Classes.FirstOrder as FOF
@@ -18,7 +17,7 @@
 import Data.Logic.Classes.Pretty (HasFixity(..), Fixity(..), FixityDirection(..))
 import qualified Data.Logic.Classes.Propositional as P
 import Data.Logic.Classes.Negate
-import Data.Logic.Harrison.Lib ({- instance Monad Failing -})
+import Data.Logic.Failing (Failing(..))
 import Text.PrettyPrint (Doc, (<>), text, parens, nest)
 
 -- |Literals are the building blocks of the clause and implicative normal
diff --git a/Data/Logic/Failing.hs b/Data/Logic/Failing.hs
new file mode 100644
--- /dev/null
+++ b/Data/Logic/Failing.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE  DeriveDataTypeable, StandaloneDeriving #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module Data.Logic.Failing
+    ( Failing(Success, Failure)
+    , failing
+    ) where
+
+import Control.Applicative.Error
+import Data.Generics
+
+failing :: ([String] -> b) -> (a -> b) -> Failing a -> b
+failing f _ (Failure errs) = f errs
+failing _ f (Success a)    = f a
+
+instance Monad Failing where
+  return = Success
+  m >>= f =
+      case m of
+        (Failure errs) -> (Failure errs)
+        (Success a) -> f a
+  fail errMsg = Failure [errMsg]
+
+deriving instance Typeable1 Failing
+deriving instance Data a => Data (Failing a)
+deriving instance Read a => Read (Failing a)
+deriving instance Eq a => Eq (Failing a)
+deriving instance Ord a => Ord (Failing a)
diff --git a/Data/Logic/Harrison/Lib.hs b/Data/Logic/Harrison/Lib.hs
--- a/Data/Logic/Harrison/Lib.hs
+++ b/Data/Logic/Harrison/Lib.hs
@@ -1,8 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable, RankNTypes, StandaloneDeriving #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-binds #-}
 module Data.Logic.Harrison.Lib
-    ( failing
-    , tests
+    ( tests
     , setAny
     , setAll
     -- , itlist2
@@ -35,35 +34,12 @@
     , (∅)
     ) where
 
-import Control.Applicative.Error (Failing(..), ErrorMsg)
-import Data.Generics
+import Data.Logic.Failing (Failing(..), failing)
 import qualified Data.Map as Map
 import Data.Maybe
 import qualified Data.Set as Set
 import Test.HUnit (Test(TestCase, TestList, TestLabel), assertEqual)
 
--- | Case analysis for the 'Failing' type, from unpublished changes to 
--- the applicative-extras packages.  If the value is @'Failure'@, apply 
--- the first function to @[ErrorMsg]@; if it is @'Success' a@, apply 
--- the second function to @a@.
-failing :: ([ErrorMsg] -> b) -> (a -> b) -> Failing a -> b
-failing f _ (Failure errs) = f errs
-failing _ f (Success a)    = f a
- 
-instance Monad Failing where
-  return = Success
-  m >>= f =
-      case m of
-        (Failure errs) -> (Failure errs)
-        (Success a) -> f a
-  fail errMsg = Failure [errMsg]
-  
-deriving instance Typeable1 Failing
-deriving instance Data a => Data (Failing a)
-deriving instance Read a => Read (Failing a)
-deriving instance Eq a => Eq (Failing a)
-deriving instance Ord a => Ord (Failing a)
-
 (∅) :: Set.Set a
 (∅) = Set.empty
 
@@ -117,6 +93,7 @@
 -- let can f x = try f x; true with Failure _ -> false;;
 can :: (t -> Failing a) -> t -> Bool
 can f x = failing (const True) (const False) (f x)
+
 {-
 let rec repeat f x = try repeat f (f x) with Failure _ -> x;;
 
diff --git a/Data/Logic/Harrison/Normal.hs b/Data/Logic/Harrison/Normal.hs
--- a/Data/Logic/Harrison/Normal.hs
+++ b/Data/Logic/Harrison/Normal.hs
@@ -15,7 +15,8 @@
 import Data.Logic.Classes.Formula (Formula(atomic))
 import Data.Logic.Classes.Literal (Literal, fromFirstOrder)
 import Data.Logic.Classes.Negate (Negatable, negated, (.~.))
-import Data.Logic.Harrison.Lib (setAny, allpairs, failing)
+import Data.Logic.Failing (failing)
+import Data.Logic.Harrison.Lib (setAny, allpairs)
 import Data.Logic.Harrison.Skolem (nnf)
 import qualified Data.Set.Extra as Set
 import Prelude hiding (negate)
diff --git a/Data/Logic/Harrison/PropExamples.hs b/Data/Logic/Harrison/PropExamples.hs
--- a/Data/Logic/Harrison/PropExamples.hs
+++ b/Data/Logic/Harrison/PropExamples.hs
@@ -352,7 +352,7 @@
 -- For large examples, should use "num" instead of "int" in these functions. 
 -- ------------------------------------------------------------------------- 
 
-bitlength :: forall b a. (Bits b, Num a) => b -> a
+bitlength :: forall b a. (Num a, Num b, Bits b) => b -> a
 bitlength x = if x == 0 then 0 else 1 + bitlength (shiftR x 1);;
 
 bit :: forall a b. (Num a, Eq a, Bits b, Integral b) => a -> b -> Bool
diff --git a/Data/Logic/Harrison/Resolution.hs b/Data/Logic/Harrison/Resolution.hs
--- a/Data/Logic/Harrison/Resolution.hs
+++ b/Data/Logic/Harrison/Resolution.hs
@@ -8,7 +8,6 @@
     , matchAtomsEq
     ) where
 
-import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Atom (Atom(match))
 import Data.Logic.Classes.Combine (Combination(..))
 import Data.Logic.Classes.Equals (AtomEq, zipAtomsEq)
@@ -18,9 +17,10 @@
 import Data.Logic.Classes.Propositional (PropositionalFormula)
 import Data.Logic.Classes.Term (Term(vt, foldTerm))
 import Data.Logic.Classes.Variable (Variable(prefix))
+import Data.Logic.Failing (Failing(..), failing)
 import Data.Logic.Harrison.FOL (subst, fv, generalize, list_disj, list_conj)
 import Data.Logic.Harrison.Lib (settryfind, allpairs, allsubsets, setAny, setAll,
-                                allnonemptysubsets, (|->), apply, defined, failing)
+                                allnonemptysubsets, (|->), apply, defined)
 import Data.Logic.Harrison.Normal (simpdnf, simpcnf, trivial)
 import Data.Logic.Harrison.Skolem (pnf, SkolemT, askolemize, specialize)
 import Data.Logic.Harrison.Tableaux (unify_literals)
diff --git a/Data/Logic/Harrison/Unif.hs b/Data/Logic/Harrison/Unif.hs
--- a/Data/Logic/Harrison/Unif.hs
+++ b/Data/Logic/Harrison/Unif.hs
@@ -6,9 +6,8 @@
     , unifyAndApply
     ) where
 
-import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Term (Term(..), tsubst)
-import Data.Logic.Harrison.Lib (failing)
+import Data.Logic.Failing (Failing(..), failing)
 import qualified Data.Map as Map
 {-
 (* ========================================================================= *)
@@ -34,6 +33,7 @@
           if any (failing (const False) id . isTrivial env x) args
           then Failure ["cyclic"]
           else Success False
+
 {-
     foldT (\ y -> y == x || (defined env y && istriv env x (apply env y)))
           (\ _ args -> if any (istriv env x) args then error "cyclic" else False)
diff --git a/Data/Logic/Tests/Harrison/Unif.hs b/Data/Logic/Tests/Harrison/Unif.hs
--- a/Data/Logic/Tests/Harrison/Unif.hs
+++ b/Data/Logic/Tests/Harrison/Unif.hs
@@ -4,9 +4,8 @@
     ( tests
     ) where
 
-import Control.Applicative.Error (Failing(..))
 import Data.Logic.Classes.Term (Term(fApp, vt), tsubst)
-import Data.Logic.Harrison.Lib (failing)
+import Data.Logic.Failing (Failing(..), failing)
 import Data.Logic.Harrison.Unif (fullUnify)
 import Data.Logic.Tests.HUnit ()
 import Data.Logic.Types.Harrison.FOL (TermType)
diff --git a/logic-classes.cabal b/logic-classes.cabal
--- a/logic-classes.cabal
+++ b/logic-classes.cabal
@@ -1,5 +1,5 @@
 Name:             logic-classes
-Version:          1.4.6
+Version:          1.4.7
 Synopsis:         Framework for propositional and first order logic, theorem proving
 Description:      Package to support Propositional and First Order Logic.  It includes classes
                   representing the different types of formulas and terms, some instances of
@@ -34,6 +34,7 @@
                    Data.Logic.Classes.Skolem
                    Data.Logic.Classes.Term
                    Data.Logic.Classes.Variable
+                   Data.Logic.Failing
                    Data.Logic.Harrison.DefCNF
                    Data.Logic.Harrison.DP
                    Data.Logic.Harrison.Equal
@@ -70,13 +71,15 @@
                    Data.Logic.Types.Harrison.Formulas.Propositional
                    Data.Logic.Types.Harrison.Prop
                    Data.Logic.Types.Propositional
- Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit, incremental-sat-solver,
+                   Data.Boolean
+                   Data.Boolean.SatSolver
+ Build-Depends:    applicative-extras, base >= 4.3 && < 5, containers, fgl, HUnit,
                    mtl, syb-with-class, text, PropLogic >= 0.9.0.3, pretty, safecopy, set-extra, syb, template-haskell
 
 Executable tests
  GHC-Options: -Wall -O2
  Main-Is: Data/Logic/Tests/Main.hs
- Build-Depends: applicative-extras, base, containers, HUnit, incremental-sat-solver, mtl,
+ Build-Depends: applicative-extras, base, containers, HUnit, mtl,
                 pretty, PropLogic, safecopy, set-extra, syb, template-haskell
  Other-Modules:    Data.Logic.Tests.Chiou0
                    Data.Logic.Tests.Common