diff --git a/Satchmo/Binary/Op/Common.hs b/Satchmo/Binary/Op/Common.hs
--- a/Satchmo/Binary/Op/Common.hs
+++ b/Satchmo/Binary/Op/Common.hs
@@ -17,6 +17,8 @@
 
 import Satchmo.Counting
 
+import Control.Monad ( forM )
+
 iszero :: (MonadSAT m) =>  Number -> m Boolean
 iszero a = equals a $ make []
 
@@ -26,13 +28,12 @@
 
 
 equals' :: (MonadSAT m) =>  Booleans -> Booleans -> m Boolean
-equals' [] [] = B.constant True
-equals' (x:xs) (y:ys) = do
-    z <- xor [x, y]
-    rest <- equals' xs ys
-    and [ not z, rest ]
-equals' xs [] = and $ map not xs
-equals' [] ys = and $ map not ys
+equals' xs ys = do
+    let n = min ( length xs ) ( length ys )
+        (a,b) = splitAt n xs
+        (c,d) = splitAt n ys
+    ac <- forM ( zip a c ) $ \ (x,y) -> fun2 (==) x y
+    and $ map not (b++d) ++ ac
 
 le,lt,ge,gt,eq :: MonadSAT m => Number -> Number -> m Boolean
 le x y = do (l,e) <- compare x y ; or [l,e]
@@ -71,9 +72,35 @@
 
 full_adder :: (MonadSAT m) 
            => Boolean -> Boolean -> Boolean
-           -> m ( Boolean, Boolean )
-full_adder p1 p2 p3 = do
+           -> m ( Boolean , Boolean ) -- ^ (result, carry)
+full_adder = full_adder_1
+
+full_adder_1 p1 p2 p3 = do
     p4 <- boolean ; p5 <- boolean
+    assert [not p1, not p2, p5]
+    assert [not p1, not p3, p5]
+    assert [not p1, p4, p5]
+    assert [p1, p2, not p5]
+    assert [p1, p3, not p5]
+    assert [p1, not p4, not p5]
+    assert [not p2, not p3, p5]
+    assert [not p2, p4, p5]
+    assert [p2, p3, not p5]
+    assert [p2, not p4, not p5]
+    assert [not p3, p4, p5]
+    assert [p3, not p4, not p5]
+    assert [not p1, not p2, not p3, p4]
+    assert [not p1, not p2, p3, not p4]
+    assert [not p1, p2, not p3, not p4]
+    assert [not p1, p2, p3, p4]
+    assert [p1, not p2, not p3, not p4]
+    assert [p1, not p2, p3, p4]
+    assert [p1, p2, not p3, p4]
+    assert [p1, p2, p3, not p4]
+    return ( p4, p5 )
+       
+full_adder_0 p1 p2 p3 = do
+    p4 <- boolean ; p5 <- boolean
     assert [not p2,p4,p5]
     assert [p2,not p4,not p5]
     assert [not p1,not p3,p5]
@@ -94,8 +121,24 @@
 
 half_adder :: (MonadSAT m) 
            => Boolean -> Boolean 
-           -> m ( Boolean, Boolean )
-half_adder p1 p2 = do
+           -> m ( Boolean, Boolean ) -- ^ (result, carry)
+half_adder = half_adder_1
+
+half_adder_1 p1 p2 = do
+    p3 <- boolean ; p4 <- boolean
+    assert [p1, not p4]
+    assert [p2, not p4]
+    assert [not p3, not p4]
+    assert [not p1, not p2, not p3]
+    assert [not p1, not p2, p4]
+    assert [not p1, p2, p3]
+    assert [not p1, p3, p4]
+    assert [p1, not p2, p3]
+    assert [p1, p2, not p3]
+    assert [not p2, p3, p4]
+    return (p3,p4)
+
+half_adder_0 p1 p2 = do
     p3 <- boolean ; p4 <- boolean
     assert [not p2,p3,p4]
     assert [p2,not p4]
diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs
--- a/Satchmo/Boolean/Data.hs
+++ b/Satchmo/Boolean/Data.hs
@@ -18,18 +18,19 @@
 import Satchmo.Data
 import Satchmo.MonadSAT
 
-import Data.Map ( Map )
-import qualified Data.Map as M
+import Satchmo.SAT (SAT) -- for specializations
+
+import Data.Array
 import Data.Maybe ( fromJust )
 import Data.List ( partition )
 
 import Control.Monad.Reader
 
 data Boolean = Boolean
-             { encode :: Literal
-             , decode :: C.Decoder Bool
+             { encode :: ! Literal
+             -- , decode :: ! ( C.Decoder Bool )
              }
-     | Constant { value :: Bool }
+     | Constant { value :: ! Bool }
 
 {-
 
@@ -65,49 +66,63 @@
 
 instance C.Decode Boolean Bool where 
     decode b = case b of
-        Boolean {} -> decode b
+        -- Boolean {} -> decode b
+        Boolean {} -> asks $ \ arr -> 
+              let x = encode b
+              in  positive x == arr ! ( variable x )
         Constant {} -> return $ value b
 
 boolean :: MonadSAT m => m Boolean
 boolean = exists
+{-# INLINABLE boolean #-}
+{-# specialize inline boolean :: SAT Boolean #-}
 
 exists :: MonadSAT m => m Boolean
+{-# specialize inline exists :: SAT Boolean #-}
 exists = do
     x <- fresh
     return $ Boolean 
            { encode = x
+{-                      
            , decode = asks $ \ fm -> 
                       ( positive x == )
                     $ fromJust
                     $ M.lookup ( variable x ) fm
+-}
            }
 
 forall :: MonadSAT m => m Boolean
+{-# specialize inline forall :: SAT Boolean #-}
 forall = do
     x <- fresh_forall
     return $ Boolean 
            { encode = x
-           , decode = error "Boolean.forall cannot be decoded"
+--           , decode = error "Boolean.forall cannot be decoded"
            }
 
 constant :: MonadSAT m => Bool -> m Boolean
+{-# specialize inline constant :: Bool -> SAT Boolean #-}
 constant v = do
     return $ Constant { value = v } 
+{-# INLINABLE constant #-}
 
 not :: Boolean -> Boolean
 not b = case b of
     Boolean {} -> Boolean 
       { encode = nicht $ encode b
-      , decode = do x <- decode b ; return $ Prelude.not x
+      -- , decode = do x <- decode b ; return $ Prelude.not x
       }
     Constant {} -> Constant { value = Prelude.not $ value b }
+{-# INLINABLE not #-}
 
 
 assert :: MonadSAT m => [ Boolean ] -> m ()
+{-# specialize inline assert :: [ Boolean ] -> SAT () #-}
 assert bs = do
     let ( con, uncon ) = partition isConstant bs
     let cval = Prelude.or $ map value con
     when ( Prelude.not cval ) $ emit $ clause $ map encode uncon
+{-# INLINABLE assert #-}
 
 assertW :: MonadSAT m => Weight -> [ Boolean ] -> m ()
 assertW w bs = do
@@ -118,7 +133,8 @@
 monadic :: Monad m
         => ( [ a ] -> m b )
         -> ( [ m a ] -> m b )
+{-# specialize inline monadic :: ([a] -> SAT b) -> [SAT a] -> SAT b #-}        
 monadic f ms = do
     xs <- sequence ms
     f xs
-
+{-# INLINABLE monadic #-}
diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs
--- a/Satchmo/Boolean/Op.hs
+++ b/Satchmo/Boolean/Op.hs
@@ -15,9 +15,12 @@
 import Satchmo.Code
 import Satchmo.Boolean.Data
 
+import Satchmo.SAT ( SAT) -- for specializations
+
 import Control.Monad ( foldM )
 
 and :: MonadSAT m => [ Boolean ] -> m Boolean
+{-# specialize inline and :: [ Boolean ] -> SAT Boolean #-}
 and [] = constant True
 and [x]= return x
 and xs = do
@@ -29,6 +32,7 @@
     return y
 
 or :: MonadSAT m => [ Boolean ] -> m Boolean
+{-# specialize inline or :: [ Boolean ] -> SAT Boolean #-}
 or [] = constant False
 or [x]= return x
 or xs = do
@@ -36,6 +40,7 @@
     return $ not y
 
 xor :: MonadSAT m => [ Boolean ] -> m Boolean
+{-# specialize inline xor :: [ Boolean ] -> SAT Boolean #-}
 xor [] = constant False
 xor (x:xs) = foldM xor2 x xs
 
@@ -46,6 +51,7 @@
         ( Bool -> Bool -> Bool )
      -> Boolean -> Boolean 
      -> m Boolean
+{-# specialize inline fun2 :: (Bool -> Bool -> Bool) -> Boolean -> Boolean -> SAT Boolean #-}
 fun2 f x y = do
     r <- boolean
     sequence_ $ do
@@ -62,6 +68,7 @@
         ( Bool -> Bool -> Bool -> Bool )
      -> Boolean -> Boolean -> Boolean
      -> m Boolean
+{-# specialize inline fun3 :: (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> SAT Boolean #-}
 fun3 f x y z = do
     r <- boolean
     sequence_ $ do
@@ -76,7 +83,9 @@
     return r
 
 xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
+{-# specialize inline  xor2 :: Boolean -> Boolean -> SAT Boolean #-}
 xor2 = fun2 (/=)
+-- xor2 = xor2_orig
 
 -- for historic reasons:
 xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean
diff --git a/Satchmo/Code.hs b/Satchmo/Code.hs
--- a/Satchmo/Code.hs
+++ b/Satchmo/Code.hs
@@ -10,17 +10,17 @@
 
 import Satchmo.Data
 
-
-import Data.Map ( Map )
-import qualified Data.Map as M
 import Data.Array
 
 import Control.Monad.Reader
 
 
-class Decode c a where decode :: c -> Decoder a
+class Decode c a where 
+    {-# INLINABLE decode #-}
+    decode :: c -> Decoder a
 
-type Decoder a = Reader ( Map Variable Bool ) a
+-- type Decoder a = Reader ( Map Variable Bool ) a
+type Decoder a = Reader ( Array Variable Bool ) a
 
 instance Decode () () where
     decode () = return ()
diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs
--- a/Satchmo/Data.hs
+++ b/Satchmo/Data.hs
@@ -43,17 +43,20 @@
 literal :: Bool -> Variable -> Literal
 literal p v | v /= 0 = 
     Literal $ if p then v else negate v
-
+{-# INLINE literal #-}
 
 nicht :: Literal -> Literal
 nicht ( Literal i ) = Literal $ negate i
+{-# INLINE nicht #-}
 
 -- FIXME: should be newtype
 type Variable = Int
 
 variable :: Literal -> Variable
 variable ( Literal v ) = abs v
+{-# INLINE variable #-}
 
 positive :: Literal -> Bool
 positive ( Literal v ) = 0 < v
 
+{-# INLINE positive #-}
diff --git a/Satchmo/MonadSAT.hs b/Satchmo/MonadSAT.hs
--- a/Satchmo/MonadSAT.hs
+++ b/Satchmo/MonadSAT.hs
@@ -5,6 +5,7 @@
 module Satchmo.MonadSAT
 
 ( MonadSAT(..), Weight
+, Header (..)                
 )
 
 where
@@ -27,9 +28,21 @@
 
 class (Functor m, Monad m) => MonadSAT m where
   fresh, fresh_forall :: m Literal
+  {-# INLINABLE fresh #-}
   emit  :: Clause -> m ()
+  {-# INLINABLE emit #-}
   emitW :: Weight -> Clause -> m ()
+  -- | emit some note (could be printed by the backend)
+  note :: String -> m ()
 
+type NumClauses = Integer
+type NumVars    = Integer
+
+data Header = 
+     Header { numClauses, numVars :: ! Int
+            , universals :: ! [Int]
+                     }
+     deriving Show
 
 -- -------------------------------------------------------
 -- MonadSAT liftings for standard monad transformers
diff --git a/Satchmo/Relation/Data.hs b/Satchmo/Relation/Data.hs
--- a/Satchmo/Relation/Data.hs
+++ b/Satchmo/Relation/Data.hs
@@ -12,15 +12,18 @@
 import Satchmo.Code
 import Satchmo.Boolean
 
+import Satchmo.SAT
+
 import qualified Data.Array as A
 import Data.Array hiding ( bounds, (!), indices, assocs )
 
 import Control.Monad ( guard )
 
-data Relation a b = Relation ( Array (a,b) Boolean ) 
+newtype Relation a b = Relation ( Array (a,b) Boolean ) 
 
 relation :: ( Ix a, Ix b, MonadSAT m ) 
          => ((a,b),(a,b)) -> m ( Relation a b ) 
+{-# specialize inline relation :: ( Ix a, Ix b) => ((a,b),(a,b)) -> SAT ( Relation a b ) #-} 
 relation bnd = do
     pairs <- sequence $ do 
         p <- range bnd
diff --git a/Satchmo/Relation/Op.hs b/Satchmo/Relation/Op.hs
--- a/Satchmo/Relation/Op.hs
+++ b/Satchmo/Relation/Op.hs
@@ -22,6 +22,8 @@
 import Control.Monad ( guard )
 import Data.Ix
 
+import Satchmo.SAT
+
 mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a
 mirror r = 
     let ((a,b),(c,d)) = bounds r
@@ -34,6 +36,7 @@
 union :: ( Ix a , Ix b, MonadSAT m ) 
       => Relation a b -> Relation a b 
       -> m ( Relation a b )
+{-# specialize inline union :: ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-}      
 union r s = do
     pairs <- sequence $ do
         i <- indices r
@@ -42,6 +45,7 @@
 
 product :: ( Ix a , Ix b, Ix c, MonadSAT m ) 
         => Relation a b -> Relation b c -> m ( Relation a c )
+{-# specialize inline product ::  ( Ix a , Ix b, Ix c ) => Relation a b -> Relation b c -> SAT ( Relation a c ) #-}      
 product a b = do
     let ((ao,al),(au,ar)) = bounds a
         ((bo,bl),(bu,br)) = bounds b
@@ -58,6 +62,7 @@
 intersection :: ( Ix a , Ix b, MonadSAT m ) 
       => Relation a b -> Relation a b 
       -> m ( Relation a b )
+{-# specialize inline intersection ::  ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-} 
 intersection r s = do
     pairs <- sequence $ do
         i <- indices r
diff --git a/Satchmo/Relation/Prop.hs b/Satchmo/Relation/Prop.hs
--- a/Satchmo/Relation/Prop.hs
+++ b/Satchmo/Relation/Prop.hs
@@ -22,29 +22,36 @@
 import Control.Monad ( guard )
 import Data.Ix
 
+import Satchmo.SAT
+
 implies :: ( Ix a, Ix b, MonadSAT m ) 
         => Relation a b -> Relation a b -> m Boolean
+{-# specialize inline implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean #-}      
 implies r s = monadic and $ do
     i <- indices r
     return $ or [ not $ r ! i, s ! i ]
 
 
 symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
+{-# specialize inline symmetric :: ( Ix a ) => Relation a a -> SAT Boolean #-}      
 symmetric r = implies r ( mirror r )
 
 irreflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
+{-# specialize inline irreflexive :: ( Ix a ) =>  Relation a a -> SAT Boolean #-}      
 irreflexive r = and $ do
     let ((a,b),(c,d)) = bounds r
     x <- range ( a, c)
     return $ Satchmo.Boolean.not $ r ! (x,x) 
 
 reflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
+{-# specialize inline reflexive :: ( Ix a ) => Relation a a -> SAT Boolean #-}      
 reflexive r = and $ do
     let ((a,b),(c,d)) = bounds r
     x <- range (a,c)
     return $ r ! (x,x) 
 
 regular :: ( Ix a, MonadSAT m) => Int -> Relation a a -> m Boolean
+{-# specialize inline regular :: ( Ix a ) => Int -> Relation a a -> SAT Boolean #-}      
 regular deg r = monadic and $ do
     let ((a,b),(c,d)) = bounds r
     x <- range ( a , c )
@@ -54,6 +61,7 @@
 
 transitive :: ( Ix a, MonadSAT m ) 
            => Relation a a -> m Boolean
+{-# specialize inline transitive :: ( Ix a ) => Relation a a -> SAT Boolean #-}      
 transitive r = do
     r2 <- product r r
     implies r2 r
diff --git a/Satchmo/SAT.hs b/Satchmo/SAT.hs
--- a/Satchmo/SAT.hs
+++ b/Satchmo/SAT.hs
@@ -1,101 +1,9 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
-module Satchmo.SAT
-
-( SAT, Header(..)
-, fresh, fresh_forall
-, emit, Weight
-, sat
-)
-
-where
-
-import Satchmo.Data
-import Satchmo.MonadSAT
-
-import Control.Exception
-import Control.Monad.RWS.Strict
-import qualified  Data.Set as Set
-import qualified Data.ByteString.Lazy.Char8 as BS
-import System.Directory
-import System.Environment
-import System.IO
-
-
-instance MonadSAT SAT where
-  fresh = satfresh
-  fresh_forall = satfresh_forall
-  emit    = satemit
-  emitW _ _ = return ()
-
--- ---------------
--- Implementation
--- ---------------
-
-data Accu = Accu
-          { next :: ! Int
-          , universal :: [Int]
-          , size :: ! Int
-          }
-
-start :: Accu
-start = Accu
-      { next = 1
-      , universal = []
-      , size = 0
-      }
-
-newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}
-    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor)
-
-type NumClauses = Integer
-type NumVars    = Integer
-
-data Header = Header { numClauses, numVars :: Int
-                     , universals :: [Int]
-                     }
-
-
-sat :: SAT a -> IO (BS.ByteString, Header, a )
-sat (SAT m) =
- bracket
-    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))
-    (\(fp, h) -> removeFile fp)
-    (\(fp, h) -> do
-       hSetBuffering h (BlockBuffering Nothing)
-       ~(a, accu, _) <- runRWST m h start
-       hClose h
-       let header = Header (size accu) (next accu - 1) universals
-           universals = reverse $ universal accu
-
-       bs <- BS.readFile fp
-       return (bs, header, a))
-
--- | existentially quantified (implicitely so, before first fresh_forall)
-satfresh :: SAT Literal
-satfresh = do
-    a <- get
-    let n = next a
-    put $ a { next = n + 1 }
-    return $ literal True n
-
--- | universally quantified
-satfresh_forall :: SAT Literal
-satfresh_forall = do
-    a <- get
-    let n = next a
-    put $ a { next = n + 1, universal = n : universal a }
-    return $ literal True n
-
-satemit :: Clause -> SAT ()
-satemit clause = do
-    a <- get
-    tellSat (bshowClause clause)
-    put $ a
-        { size = size a + 1
-        }
-  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
-
-
-tellSat x = do {h <- ask; liftIO $ BS.hPut h x}
+module Satchmo.SAT ( 
+  -- module Satchmo.SAT.BS 
+  -- module Satchmo.SAT.Seq
+  module Satchmo.SAT.Tmpfile
+) where
 
+import Satchmo.SAT.Seq
+import Satchmo.SAT.BS
+import Satchmo.SAT.Tmpfile
diff --git a/Satchmo/SAT/BS.hs b/Satchmo/SAT/BS.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/BS.hs
@@ -0,0 +1,67 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Satchmo.SAT.BS
+
+( SAT, Header(..)
+, fresh, fresh_forall
+, emit, Weight
+, sat
+)
+
+where
+
+import Satchmo.Data
+import Satchmo.MonadSAT
+
+import Control.Exception
+
+import Control.Monad.RWS.Strict
+-- import Control.Monad.RWS.Lazy
+
+-- import qualified Data.ByteString.Lazy.Char8 as BS
+import qualified Data.ByteString.Char8 as BS
+
+import Data.Foldable
+import Data.String
+
+newtype SAT a 
+      = SAT { unSAT :: -- WriterT BS.ByteString ( StateT Header Identity ) 
+                       -- StateT Header ( WriterT BS.ByteString Identity )
+                       RWS () BS.ByteString Header
+                       -- RWS () ( S.Seq BS.ByteString ) Header
+                       a
+            } 
+      deriving ( Functor, Monad
+               , MonadState Header
+               , MonadWriter BS.ByteString
+               -- , MonadWriter ( S.Seq BS.ByteString )
+               )
+
+
+instance MonadSAT SAT where
+  fresh = do 
+      a <- get 
+      let v = numVars a
+      put $ a { numVars = succ v } 
+      return $ literal True $ succ v
+  emit cl = do
+      a <- get
+      put $ a { numClauses = succ $ numClauses a }
+      tell $  fromString $ show  cl ++ "\n"
+  note msg = do
+      return ()
+     
+start :: Header
+start = Header { numClauses = 0, numVars = 0
+               , universals = []
+               }
+
+
+sat :: SAT a -> IO (BS.ByteString, Header, a )
+sat (SAT m) = do
+    let -- ((res,bs),accu) = runState (runWriterT m) start
+        -- ((res,accu),bs) = runWriter ( runStateT m  start )
+        (res, accu, bs) = runRWS m () start 
+    return ( bs , accu, res )
+
+
diff --git a/Satchmo/SAT/Seq.hs b/Satchmo/SAT/Seq.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/Seq.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Satchmo.SAT.Seq
+
+( SAT, Header(..)
+, fresh, fresh_forall
+, emit, Weight
+, sat
+)
+
+where
+
+import Satchmo.Data
+import Satchmo.MonadSAT
+
+import Control.Exception
+
+import Control.Monad.RWS.Strict
+-- import Control.Monad.RWS.Lazy
+
+-- import qualified Data.Sequence as S
+import qualified Satchmo.SAT.Sequence as S
+
+import qualified Data.ByteString.Char8 as BS
+-- import qualified Data.ByteString.Lazy.Char8 as BS
+
+import Data.Foldable
+import Data.String
+
+newtype SAT a 
+      = SAT { unSAT :: -- WriterT BS.ByteString ( StateT Header Identity ) 
+                       -- StateT Header ( WriterT BS.ByteString Identity )
+                       -- RWS () BS.ByteString Header
+                       RWS () ( S.Seq BS.ByteString ) Header
+                       a
+            } 
+      deriving ( Functor, Monad
+               , MonadState Header
+               , MonadWriter ( S.Seq BS.ByteString )
+               -- , MonadWriter BS.ByteString
+               )
+
+
+instance MonadSAT SAT where
+  note msg = do return ()
+  fresh = do 
+      a <- get 
+      let v = numVars a
+      put $ a { numVars = succ v } 
+      return $ literal True $ succ v
+  emit cl = do
+      a <- get
+      put $ a { numClauses = succ $ numClauses a }
+      tell $  S.singleton $ fromString $ show  cl ++ "\n"
+
+     
+start :: Header
+start = Header { numClauses = 0, numVars = 0
+               , universals = []
+               }
+
+
+sat :: SAT a -> IO (BS.ByteString, Header, a )
+sat (SAT m) = do
+    let -- ((res,bs),accu) = runState (runWriterT m) start
+        -- ((res,accu),bs) = runWriter ( runStateT m  start )
+        (res, accu, bs) = runRWS m () start 
+    return ( fold bs , accu, res )
+
+
diff --git a/Satchmo/SAT/Sequence.hs b/Satchmo/SAT/Sequence.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/Sequence.hs
@@ -0,0 +1,26 @@
+-- | binary trees without any balance
+
+module Satchmo.SAT.Sequence where
+
+import Data.Monoid
+import Data.Foldable
+
+data Seq a = Empty | Leaf !a 
+           | Branch !(Seq a) !(Seq a)
+
+{-# INLINABLE singleton #-}
+singleton x = Leaf x
+
+instance Monoid (Seq a) where
+    {-# INLINABLE mappend #-}
+    mappend = Branch
+    {-# INLINABLE mempty #-}
+    mempty = Empty
+
+instance Foldable Seq where
+    {-# INLINABLE fold #-}
+    fold s = case s of
+        Empty -> mempty
+        Leaf k -> k
+        Branch l r -> mappend (fold l) (fold r)
+        
diff --git a/Satchmo/SAT/Tmpfile.hs b/Satchmo/SAT/Tmpfile.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/Tmpfile.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Satchmo.SAT.Tmpfile
+
+( SAT, Header(..)
+, fresh, fresh_forall
+, emit, Weight
+, sat
+)
+
+where
+
+import Satchmo.Data
+import Satchmo.MonadSAT
+
+import Control.Exception
+import Control.Monad.RWS.Strict
+import qualified  Data.Set as Set
+
+-- import qualified Data.ByteString.Lazy.Char8 as BS
+import qualified Data.ByteString.Char8 as BS
+
+import System.Directory
+import System.Environment
+import System.IO
+
+import qualified Data.Map as M
+
+import Data.List ( sortBy )
+import Data.Ord ( comparing )
+
+instance MonadSAT SAT where
+  fresh = satfresh
+  fresh_forall = satfresh_forall
+  emit    = satemit
+  emitW _ _ = return ()
+  note msg = do a <- get ; put $ a { notes = msg : notes a }
+
+-- ---------------
+-- Implementation
+-- ---------------
+
+data Accu = Accu
+          { next :: ! Int
+          , universal :: [Int]
+          , size :: ! Int
+          , notes :: ! [ String ]
+          , census :: ! ( M.Map Int Int )
+          }
+
+start :: Accu
+start = Accu
+      { next = 1
+      , universal = []
+      , size = 0
+      , notes = [ "Satchmo.SAT.Tmpfile implementation" ]
+      , census = M.empty          
+      }
+
+newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}
+    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor)
+
+
+sat :: SAT a -> IO (BS.ByteString, Header, a )
+sat (SAT m) =
+ bracket
+    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))
+    (\(fp, h) -> removeFile fp)
+    (\(fp, h) -> do
+       hSetBuffering h (BlockBuffering Nothing)
+       ~(a, accu, _) <- runRWST m h start
+       hClose h
+       
+       forM ( reverse $ notes accu ) $ hPutStrLn stderr 
+       hPutStrLn stderr $ unlines 
+           [ "(clause length, frequency)"
+           , show $ sortBy ( comparing ( negate . snd )) 
+                        $ M.toList $ census accu
+           ]  
+       
+       let header = Header (size accu) (next accu - 1) universals
+           universals = reverse $ universal accu
+
+       bs <- BS.readFile fp
+       return (bs, header, a))
+
+-- | existentially quantified (implicitely so, before first fresh_forall)
+satfresh :: SAT Literal
+satfresh = do
+    a <- get
+    let n = next a
+    put $ a { next = n + 1 }
+    return $ literal True n
+
+-- | universally quantified
+satfresh_forall :: SAT Literal
+satfresh_forall = do
+    a <- get
+    let n = next a
+    put $ a { next = n + 1, universal = n : universal a }
+    return $ literal True n
+
+satemit :: Clause -> SAT ()
+satemit clause = do
+    h <- ask ; liftIO $ hPutStrLn h $ show clause
+    a <- get
+    -- tellSat (bshowClause clause)
+    put $ a
+        { size = size a + 1
+        , census = M.insertWith (+) (length $ literals clause) 1 $ census a         
+        }
+  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
+
+
+tellSat x = do {h <- ask; liftIO $ BS.hPut h x}
+
diff --git a/Satchmo/SAT/Weighted.hs b/Satchmo/SAT/Weighted.hs
--- a/Satchmo/SAT/Weighted.hs
+++ b/Satchmo/SAT/Weighted.hs
@@ -2,13 +2,14 @@
 module Satchmo.SAT.Weighted (SAT, sat, MaxWeight, Header(..)) where
 
 import Satchmo.Data
-import Satchmo.MonadSAT
+import Satchmo.MonadSAT hiding ( Header )
 
 import Control.Exception
 import Control.Monad.RWS.Strict
 import Data.Maybe
 import qualified  Data.Set as Set
-import qualified Data.ByteString.Lazy.Char8 as BS
+-- import qualified Data.ByteString.Lazy.Char8 as BS
+import qualified Data.ByteString.Char8 as BS
 import System.Directory
 import System.Environment
 import System.IO
diff --git a/Satchmo/Solve.hs b/Satchmo/Solve.hs
--- a/Satchmo/Solve.hs
+++ b/Satchmo/Solve.hs
@@ -15,23 +15,25 @@
 import Satchmo.SAT
 import qualified Satchmo.SAT.Weighted as Weighted
 
-import qualified Data.ByteString.Lazy.Char8 as BS
+-- import qualified Data.ByteString.Lazy.Char8 as BS
+import qualified Data.ByteString.Char8 as BS
+
 import Data.Map ( Map )
 import qualified Data.Map as M
-
+import Data.Array
 import Control.Monad.Reader
 
 import System.IO
 
 type Implementation = BS.ByteString 
                     -> Header 
-                    -> IO ( Maybe ( Map Variable Bool ) )
+                    -> IO ( Maybe ( Array Variable Bool ) )
 
 type WeightedImplementation = BS.ByteString 
-                            -> Weighted.Header 
-                            -> IO ( Maybe ( Map Variable Bool ) )
+    -> Weighted.Header 
+    -> IO ( Maybe ( Array Variable Bool ) )
 
-solve :: Implementation 
+solve :: Implementation
       -> SAT ( Decoder a ) 
       -> IO ( Maybe a )
 solve implementation build = do
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        1.8.1
+Version:        1.9.1
 
 License:        GPL
 License-file:	gpl-2.0.txt
@@ -17,6 +17,7 @@
 build-type: Simple
 
 Library
+    ghc-options: -funbox-strict-fields
     Build-depends:  mtl, process, containers, base == 4.*, array, bytestring, directory
     Exposed-modules:
         Satchmo.Data
@@ -36,6 +37,10 @@
         Satchmo.Relation.Prop
         Satchmo.MonadSAT
         Satchmo.SAT
+        Satchmo.SAT.Tmpfile
+        Satchmo.SAT.BS
+        Satchmo.SAT.Seq
+        Satchmo.SAT.Sequence
         Satchmo.Simple
         Satchmo.SAT.Weighted
     Other-modules: