diff --git a/SatMicro.hs b/SatMicro.hs
new file mode 100644
--- /dev/null
+++ b/SatMicro.hs
@@ -0,0 +1,238 @@
+{-# LANGUAGE DeriveDataTypeable
+           , PatternSignatures #-}
+
+{-
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU Lesser General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    DPLLSat is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU Lesser General Public License for more details.
+
+    You should have received a copy of the GNU Lesser General Public License
+    along with DPLLSat.  If not, see <http://www.gnu.org/licenses/>.
+
+    Copyright 2008 Denis Bueno
+-}
+
+
+-- | A Haskell implementation of the basic algorithm, including
+-- non-chronological backtracking, from ''SAT-MICRO: petit mais costaud!'' by
+-- Sylvain Conchon, Johannes Kanig, and Stephane Lescuyer.
+--
+-- One interesting thing about this implementation is its use of CPS where the
+-- OCaml implementation uses exceptions, to handle control flow.
+--
+-- Optimisations:
+-- non-chronological backtracking;
+--
+-- Backtracking uses the control stack, so, you may want to invoke with
+-- something like @
+--    sat-micro cnf-file +RTS -K768M -RTS@,
+-- depending on the size of the SAT instance.
+
+module SatMicro where
+
+import Control.Monad.Cont hiding (mapM_)
+import Control.Monad.State.Strict hiding ((>=>), mapM_)
+import Data.Foldable hiding (sequence_)
+import Data.List hiding (elem, concat, foldl', foldl, any, all, foldr, maximumBy)
+import Data.Map (Map)
+import Data.Ord (comparing)
+import Data.Set (Set)
+import Debug.Trace()
+import Prelude hiding (or, and, all, any, elem, minimum, foldr, splitAt
+                      , concatMap, foldl, catch, mapM_)
+import Text.PrettyPrint.HughesPJ
+import qualified Data.Foldable as Foldable
+import qualified Data.List as L
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+
+type CNF = [[Lit]]
+
+data Result = Sat [Lit] | Unsat
+instance Show Result where
+   show (Sat lits) = "satisfiable: " ++ intercalate " " (map show lits)
+   show Unsat      = "unsatisfiable"
+
+
+newtype Lit = L {unLit :: Int} deriving (Eq, Ord)
+{-# INLINE inLit #-}
+inLit f = L . f . unLit
+
+instance Show Lit where
+    show = show . unLit
+instance Read Lit where
+    readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s :: [(Int, String)])
+
+instance Num Lit where
+    _ + _ = error "+ doesn't make sense for literals"
+    _ - _ = error "- doesn't make sense for literals"
+    _ * _ = error "* doesn't make sense for literals"
+    signum _ = error "signum doesn't make sense for literals"
+    negate   = inLit negate
+    abs      = inLit abs
+    fromInteger l | l == 0    = error "0 is not a literal"
+                  | otherwise = L $ fromInteger l
+
+
+-- | The state of the search process.
+data StateContents = S {
+      gamma :: Map Lit (Set Lit), -- ^ annotated assignment literals
+      delta :: [([Lit], Set Lit)] -- ^ annotated CNF
+    }
+
+getGamma l e = Map.findWithDefault (error $ show l ++ ": annotation not found")
+               l (gamma e)
+instance Show StateContents where
+    show = render . stateDoc
+      where
+stateDoc (S {gamma=gamma, delta=delta}) =
+    brackets (hcat . intersperse space . map (text . show) $ Map.keys gamma)
+    <+> braces (hcat
+                . intersperse (comma <> space)
+                . map (\(c, a) -> braces (hcat
+                                          . intersperse space
+                                          . map (text . show) $ c)
+                                  <> tups (hcat
+                                           . intersperse comma
+                                           . map (text . show)
+                                           $ Set.toList a))
+                $ delta)
+        where tups p = char '<' <> p <> char '>'
+
+
+-- | The entry point to the solver.  Searches for a solution to the given
+-- satisfiability problem.
+dpll :: CNF -> Result
+dpll f = (`runCont` id) $ do
+    r <- callCC $ \bj -> do
+           (Right env) <- bcp bj (initialState f)
+           unsat env return
+    either (const $ return Unsat) (return . Sat) r
+
+dispatch d = map (\l -> (l, d))
+initialState f = S {gamma = Map.empty,
+                    delta = (dispatch Set.empty f)}
+
+-- bcp either:
+--  1. finds a conflict and returns annotation literals (Left)
+--  2. computes a new environment (Right)
+
+-- | Given an annotated literal, assume it and propagate this information.
+-- This may cause other assignments to take place.
+assume :: (Monad m) =>
+          (Either (Set Lit) b -> m StateContents)
+          -> StateContents
+          -> (Lit, Set Lit)
+          -> m (Either a StateContents)
+{-# INLINE assume #-}
+assume bj env (l, s) = -- update only if not present
+    if l `Map.member` gamma env
+    then return (Right env)
+    else bcp bj env{gamma = Map.insert l s (gamma env)}
+
+-- | Boolean constraint propagation.  Under the current assignment, finds any
+-- conflicting or unit clauses, and then back jumps or assigns, respectively.
+-- If there is no conflict, computes a new environment (@Right@). If this
+-- function finds a conflict, calls @bj@ with set of literals annotating the
+-- conflicting clause (@Left@).
+bcp :: (Monad m) =>
+       (Either (Set Lit) b -> m StateContents) -- ^ for backjumping
+       -> StateContents
+       -> m (Either a StateContents)
+bcp bj env = do
+    env' <-
+        foldM (\env' (cl, a) -> do
+                 let (cl_neg, cl') =
+                         partition (\l -> negate l `Map.member` gamma env') cl
+                 if any (`Map.member` gamma env') cl'
+                  then return env'
+                  else do
+                    -- update clause annotation
+                    let a' = foldl'
+                             (\set l -> set `Set.union` getGamma (negate l) env')
+                             a cl_neg
+                    case cl' of
+                         []  -> bj (Left a')
+                         [f] -> assume bj env' (f, a') >>= return . fromRight
+                         _   -> return $ env'{delta = (cl', a'):(delta env')})
+        (env{delta = []})
+        (delta env)
+    return $ Right env'
+
+-- | @unsat@ either:
+--
+--    1. returns annotation literals (@Left@)
+--
+--    2. finds satisfying assignment (@Right@)
+unsat :: (MonadCont m) =>
+         StateContents
+         -> (Either (Set Lit) [Lit] -> m (Either (Set Lit) [Lit]))
+            -- ^ the back jump function, allowing conflicts to backtrack to
+            -- the point where the last involved literal was decided.
+         -> m (Either (Set Lit) [Lit])
+unsat env bj =
+    case delta env of
+      [] -> return $ Right $ Map.keys (gamma env)
+      ([_],_):_ -> error "unpropagated unit literal"
+      ([],_):_  -> error "conflict unresolved"
+      _ -> do
+        let a = maxSatLit (delta env)
+        r <- callCC $ \innerBj -> do
+               (Right env') <- assume innerBj env (a, Set.singleton a)
+               -- done propagating, no conflicts: continue
+               unsat env' return
+        case r of
+          Left d ->
+              if not $ a `elem` d
+              then bj (Left d)
+              else (callCC $ \innerBj -> do
+                      (Right env') <-
+                          assume innerBj env (negate a, Set.delete a d)
+                      unsat env' bj)
+                   >>= either (bj . Left) (return . Right)
+          Right _ -> bj r
+
+
+-- | Returns a literals satisfying a maximal number of clauses.
+maxSatLit cs = (`evalState` Map.empty) $ do
+  mapM_ (\(c, _) -> mapM_ incr c) cs
+  map <- get
+  return $ maximumBy (comparing (valueIn map)) lits
+    where
+      valueIn m l = Map.findWithDefault (error $ "key not found: " ++ show l) l m
+      lits = foldl (\cs' (c, _) -> cs' `L.union` c) [] cs
+
+-- * Helpers
+
+
+fromRight (Right a) = a
+fromRight (Left _)  = error "fromRight: Left"
+
+modSlot slot f = modify $ \s -> f s (slot s)
+
+incr :: (Num a) => Lit -> State (Map Lit a) ()
+{-# INLINE incr #-}
+incr l = modify $! Map.insertWith (\_ i -> 1+i) l 1
+
+paper1 :: CNF =
+  [[-1, -3, -4]
+  ,[-1, -3, 4]
+  ,[2, 3, 5]
+  ,[3, 5]
+  ,[3, -5]]
+
+
+
+-- | Verify a satisfying assignment.
+verifyResult :: Result -> CNF -> Bool
+verifyResult (Sat m) cnf =
+   -- m is well-formed
+   all (\l -> not $ negate l `elem` m) m
+   && all (\cl -> any (`elem` cl) m) cnf
+verifyResult Unsat _ = True
diff --git a/sat-micro-hs.cabal b/sat-micro-hs.cabal
--- a/sat-micro-hs.cabal
+++ b/sat-micro-hs.cabal
@@ -1,5 +1,5 @@
 Name:                sat-micro-hs
-Version:             0.1
+Version:             0.1.1
 Description:         A complete (in the logical sense) SAT solver with non-chronological backtracking.  This is a Haskell implementation of (most of) the minimal OCaml solver described in the paper "SAT-MICRO: petit mais costaud!" by Sylvain Conchon, Johannes Kanig, and Stephane Lescuyer.
 Synopsis:            A minimal SAT solver
 Category:            Algorithms
@@ -14,3 +14,4 @@
 Executable:          sat-micro
 Main-is:             Main.hs
 Ghc-options:         -W
+Other-modules:       SatMicro