diff --git a/Data/Boolean.hs b/Data/Boolean.hs
--- a/Data/Boolean.hs
+++ b/Data/Boolean.hs
@@ -75,8 +75,8 @@
 -- 
 booleanToCNF :: Boolean -> CNF
 booleanToCNF
-  = map (map literal . flatDisjunction)
-  . flatConjunction
+  = map (map literal . disjunction)
+  . conjunction
   . asLongAsPossible distribute
   . asLongAsPossible pushNots
   . asLongAsPossible elim
@@ -108,14 +108,16 @@
 
 -- private helper functions
 
-flatConjunction :: Boolean -> [Boolean]
-flatConjunction b = flat b []
- where flat (x:&&:y) = flat x . flat y
+conjunction :: Boolean -> [Boolean]
+conjunction b = flat b []
+ where flat Yes      = id
+       flat (x:&&:y) = flat x . flat y
        flat x        = (x:)
 
-flatDisjunction :: Boolean -> [Boolean]
-flatDisjunction b = flat b []
- where flat (x:||:y) = flat x . flat y
+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
diff --git a/Data/Boolean/SatSolver.hs b/Data/Boolean/SatSolver.hs
--- a/Data/Boolean/SatSolver.hs
+++ b/Data/Boolean/SatSolver.hs
@@ -23,7 +23,7 @@
 
   newSatSolver, isSolved, 
 
-  lookupVar, assertTrue, branchOnVar, satisfy, selectBranchVar
+  lookupVar, assertTrue, branchOnVar, selectBranchVar, solve
 
   ) where
 
@@ -76,22 +76,22 @@
         (const (return solver))
         (lookupVar name solver)
 
--- | 
--- 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@.
--- 
-satisfy :: MonadPlus m => SatSolver -> m SatSolver
-satisfy solver
-  | isSolved solver = return solver
-  | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= satisfy
-
 -- |
 -- 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
 
 
 -- private helper functions
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
+Version:       0.1.1
 Cabal-Version: >= 1.6
 Synopsis:      Simple, Incremental SAT Solving as a Library
 Description:   This Haskell library provides an implementation of the