diff --git a/Data/Boolean.hs b/Data/Boolean.hs
--- a/Data/Boolean.hs
+++ b/Data/Boolean.hs
@@ -21,7 +21,7 @@
 
   Literal(..), literalVar, invLiteral, isPositiveLiteral, 
 
-  CNF, booleanToCNF
+  CNF, Clause, booleanToCNF
 
   ) where
 
diff --git a/Data/Boolean/SatSolver.hs b/Data/Boolean/SatSolver.hs
--- a/Data/Boolean/SatSolver.hs
+++ b/Data/Boolean/SatSolver.hs
@@ -62,8 +62,11 @@
 -- assertion may fail if the resulting constraints are unsatisfiable.
 -- 
 assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver
-assertTrue formula solver =
-  simplify (solver { clauses = booleanToCNF formula ++ clauses solver })
+assertTrue formula solver = do
+  newClauses <- foldl (addClause (bindings solver))
+                      (return (clauses solver))
+                      (booleanToCNF formula)
+  simplify (solver { clauses = newClauses })
 
 -- |
 -- This function guesses a value for the given variable, if it is
@@ -104,6 +107,21 @@
 
 
 -- 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
diff --git a/incremental-sat-solver.cabal b/incremental-sat-solver.cabal
--- a/incremental-sat-solver.cabal
+++ b/incremental-sat-solver.cabal
@@ -1,5 +1,5 @@
 Name:          incremental-sat-solver
-Version:       0.1.6
+Version:       0.1.7
 Cabal-Version: >= 1.6
 Synopsis:      Simple, Incremental SAT Solving as a Library
 Description:   This Haskell library provides an implementation of the