diff --git a/Satchmo/Binary/Data.hs b/Satchmo/Binary/Data.hs
--- a/Satchmo/Binary/Data.hs
+++ b/Satchmo/Binary/Data.hs
@@ -29,7 +29,7 @@
 width n = length $ bits n
 
 -- | declare a number variable (bit width)
-number :: Int -> SAT Number
+number :: MonadSAT m => Int -> m Number
 number w = do
     xs <- sequence $ replicate w boolean
     return $ make xs
@@ -50,7 +50,7 @@
     in  toEnum ( fromIntegral m ) : toBinary d
 
 -- | declare a number constant 
-constant :: Integer -> SAT Number
+constant :: MonadSAT m => Integer -> m Number
 constant n = do
     xs <- mapM B.constant $ toBinary n
     return $ make xs
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
@@ -11,21 +11,21 @@
 
 import qualified Satchmo.Code as C
 
-import Satchmo.Boolean hiding ( constant )
+import Satchmo.Boolean (MonadSAT, Boolean, Booleans, fun2, fun3, and, or, not, xor, assert, boolean)
 import qualified  Satchmo.Boolean as B
-import Satchmo.Binary.Data
+import Satchmo.Binary.Data (Number, make, bits)
 
 import Satchmo.Counting
 
-iszero :: Number -> SAT Boolean
+iszero :: (MonadSAT m) =>  Number -> m Boolean
 iszero a = equals a $ make []
 
-equals :: Number -> Number -> SAT Boolean
+equals :: (MonadSAT m) =>  Number -> Number -> m Boolean
 equals a b = do
     equals' ( bits a ) ( bits b )
 
 
-equals' :: Booleans -> Booleans -> SAT Boolean
+equals' :: (MonadSAT m) =>  Booleans -> Booleans -> m Boolean
 equals' [] [] = B.constant True
 equals' (x:xs) (y:ys) = do
     z <- xor [x, y]
@@ -34,46 +34,78 @@
 equals' xs [] = and $ map not xs
 equals' [] ys = and $ map not ys
 
+le,lt,ge,gt,eq :: MonadSAT m => Number -> Number -> m Boolean
 le x y = do (l,e) <- compare x y ; or [l,e]
 lt x y = do (l,e) <- compare x y ; return l
 ge x y = le y x
 gt x y = lt y x
 eq = equals
 
-compare :: Number -> Number 
-        -> SAT ( Boolean, Boolean )
+compare :: MonadSAT m => Number -> Number 
+        -> m ( Boolean, Boolean )
 compare a b = compare' ( bits a ) ( bits b )
 
-compare' :: Booleans 
+compare' :: (MonadSAT m) => Booleans 
          -> Booleans 
-         -> SAT ( Boolean, Boolean ) -- ^ (less, equals)
+         -> m ( Boolean, Boolean ) -- ^ (less, equals)
+
 compare' [] [] = do 
-    f <- B.constant False ; t <- B.constant True ; return ( f, t )
+    f <- B.constant False 
+    t <- B.constant True 
+    return ( f, t )
 compare' (x:xs) (y:ys) = do
     l <- and [ not x, y ]
     e <- fmap not $ xor [ x, y ]
     ( ll, ee ) <- compare' xs ys
     lee <- and [l,ee]
-    l' <- or [ l, lee ] ; e' <- and [ e, ee ]
+    l' <- or [ ll, lee ]
+    e' <- and [ e, ee ]
     return ( l', e' )
 compare' xs [] = do
     x <- or xs
-    return ( not x, not x )
+    never <- B.constant False
+    return ( never, not x )
 compare' [] ys = do
     y <- or ys
     return ( y, not y )
 
-full_adder :: Boolean -> Boolean -> Boolean
-           -> SAT ( Boolean, Boolean )
-full_adder a b c = do
+full_adder :: (MonadSAT m) 
+           => Boolean -> Boolean -> Boolean
+           -> m ( Boolean, Boolean )
+full_adder 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]
+    assert [not p1,not p2,not p3,p4]
+    assert [not p1,not p2,p3,not p4]
+    assert [not p1,p2,p3,p4]
+    assert [p1,p3,not p5]
+    assert [p1,not p2,not p3,not p4]
+    assert [p1,p2,not p3,p4]
+    assert [p1,p2,p3,not p4]
+    return ( p4, p5 )
+
+full_adder_plain a b c = do
     let s x y z = sum $ map fromEnum [x,y,z]
     r <- fun3 ( \ x y z -> odd $ s x y z ) a b c
     d <- fun3 ( \ x y z -> 1   < s x y z ) a b c
     return ( r, d )
 
-half_adder :: Boolean -> Boolean 
-           -> SAT ( Boolean, Boolean )
-half_adder a b = do
+half_adder :: (MonadSAT m) 
+           => Boolean -> Boolean 
+           -> m ( Boolean, Boolean )
+half_adder p1 p2 = do
+    p3 <- boolean ; p4 <- boolean
+    assert [not p2,p3,p4]
+    assert [p2,not p4]
+    assert [not p1,p3,p4]
+    assert [not p1,not p2,not p3]
+    assert [p1,not p4]
+    assert [p1,p2,not p3]
+    return ( p3, p4 )
+
+half_adder_plain a b = do
     let s x y = sum $ map fromEnum [x,y]
     r <- fun2 ( \ x y -> odd $ s x y ) a b
     d <- fun2 ( \ x y -> 1   < s x y ) a b
diff --git a/Satchmo/Binary/Op/Fixed.hs b/Satchmo/Binary/Op/Fixed.hs
--- a/Satchmo/Binary/Op/Fixed.hs
+++ b/Satchmo/Binary/Op/Fixed.hs
@@ -27,9 +27,12 @@
 
 import Satchmo.Counting
 
+import Data.Map ( Map )
+import qualified Data.Map as M
+
 -- | give only lower k bits, upper bits must be zero,
 -- (else unsatisfiable)
-restricted :: Int -> Number -> SAT Number
+restricted :: (MonadSAT m) => Int -> Number -> m Number
 restricted w a = do
     let ( low, high ) = splitAt w $ bits a
     sequence $ do x <- high ; return $ assert [ not x ]
@@ -37,41 +40,40 @@
 
 -- | result bit width is max of argument bit widths.
 -- if overflow occurs, then formula is unsatisfiable.
-add :: Number -> Number -> SAT Number
+add :: (MonadSAT m) => Number -> Number -> m Number
 add a b = do
     false <- Satchmo.Boolean.constant False
     let w = max ( width a ) ( width b )
     zs <- add_with_carry w false ( bits a ) ( bits b )
     return $ make zs 
 
-add_with_carry :: Int -> Boolean -> Booleans -> Booleans -> SAT Booleans
+add_with_carry :: (MonadSAT m) => Int -> Boolean -> Booleans -> Booleans -> m Booleans
 add_with_carry w c xxs yys = case ( xxs, yys ) of
     _ | w <= 0 -> do
         sequence_ $ do p <- c : xxs ++ yys ; return $ assert [ not p ]
         return []
     ( [] , [] ) -> return [ c ]
     ( [], y : ys) -> do
-        -- r <- xor [ c, y ]
-        -- d <- and [ c, y ]
         (r,d) <- half_adder c y
         rest <- add_with_carry (w-1) d [] ys
         return $ r : rest
     ( x : xs, [] ) -> add_with_carry w c yys xxs
     (x : xs, y:ys) -> do
-        -- r <- xor [c,x,y]
-        -- d <- atleast 2 [c,x,y]
         (r,d) <- full_adder c x y
         rest <- add_with_carry (w-1) d xs ys
         return $ r : rest
 
 -- | result bit width is at most max of argument bit widths.
 -- if overflow occurs, then formula is unsatisfiable.
-times :: Number -> Number -> SAT Number
+times :: (MonadSAT m) => Number -> Number -> m Number
 times a b = do 
     let w = max ( width a ) ( width b ) 
-    restricted_times w a b
+    -- restricted_times w a b
+    better_times w a b
 
-restricted_times :: Int -> Number -> Number -> SAT Number
+restricted_times :: (MonadSAT m) 
+                 => Int 
+                 -> Number -> Number -> m Number
 restricted_times w a b = case bits a of
     [] -> return $ make []
     _ | w <= 0 -> do
@@ -87,8 +89,41 @@
         s <- Flexible.add xys xsys
         restricted w s
 
-        
+-------------------------------------------------- 
 
+better_times w a b = do
+    kzs <- sequence $ do
+          ( i , x ) <- zip [ 0 .. ] $ bits a
+          ( j , y ) <- zip [ 0 .. ] $ bits b
+          return $ 
+              if i+j >= w 
+              then do 
+                  assert [ not x, not y ]
+                  return ( i+j, [] )
+              else do 
+                  z <- and [ x, y ]
+                  return ( i+j , [z] ) 
+    zs <- reduce $ take w
+                 $ M.elems $ M.fromListWith (++) kzs
+    return $ make zs
 
 
+reduce ( ( x:y:z:ps) : qss ) = do
+    ( r, c ) <- full_adder x y z
+    qss' <- plugin c qss
+    reduce $ ( ps ++ [r] ) : qss' 
+reduce ( ( x:y:[]) : qss ) = do
+    ( r, c ) <- half_adder x y 
+    qss' <- plugin c qss
+    reduce $ [r] : qss' 
+reduce ( ( x:[]) : qss ) = do
+    xs <- reduce qss
+    return $ x : xs
+reduce [] = return []
+
+plugin c [] = do
+    assert [ not c ]
+    return []
+plugin c (qs : qss) = 
+    return ((c:qs) : qss)
 
diff --git a/Satchmo/Binary/Op/Flexible.hs b/Satchmo/Binary/Op/Flexible.hs
--- a/Satchmo/Binary/Op/Flexible.hs
+++ b/Satchmo/Binary/Op/Flexible.hs
@@ -21,47 +21,82 @@
 import Satchmo.Binary.Op.Common
 import Satchmo.Counting
 
-add :: Number -> Number -> SAT Number
+import qualified Data.Map as M
+
+add :: (MonadSAT m) => Number -> Number -> m Number
 add a b = do
     false <- Satchmo.Boolean.constant False
-    ( zs, carry ) <- add_with_carry false (bits a) (bits b)
+    ( zs, carry ) <- 
+        add_with_carry false (bits a) (bits b)
     return $ make $ zs ++ [carry]
 
-add_with_carry :: Boolean 
+add_with_carry :: (MonadSAT m) => Boolean 
                -> Booleans -> Booleans
-               -> SAT ( Booleans, Boolean )
+               -> m ( Booleans, Boolean )
 add_with_carry cin [] [] = return ( [], cin )
 add_with_carry cin (x:xs) [] = do
-    -- z <- xor [ cin, x ]
-    -- c <- and [ cin, x ]
     (z, c) <- half_adder cin x
     ( zs, cout ) <- add_with_carry c xs []
     return ( z : zs, cout )
 add_with_carry cin [] (y:ys) = do
     add_with_carry cin (y:ys) []
 add_with_carry cin (x:xs ) (y:ys) = do
-    -- z  <- xor [ cin, x, y ]
-    -- c <- atleast 2 [ cin, x, y ]
     (z, c) <- full_adder cin x y
     ( zs, cout ) <- add_with_carry c xs ys
     return ( z : zs, cout )
 
-times :: Number -> Number -> SAT Number
-times a b | [x] <- bits a = times1 x b
-times a b | x:xs <- bits a = do
+times :: (MonadSAT m) => Number -> Number -> m Number
+times = better_times
+
+plain_times :: (MonadSAT m) => Number -> Number -> m Number
+plain_times a b | [] <- bits a = return a
+plain_times a b | [] <- bits b = return b
+plain_times a b | [x] <- bits a = times1 x b
+plain_times a b | [y] <- bits b = times1 y a
+plain_times a b | x:xs <- bits a = do
     xys  <- times1 x b
-    xsys <- times (make xs) b
+    xsys <- plain_times (make xs) b
     zs <- shift xsys
     add xys zs
 
 -- | multiply by 2
-shift :: Number -> SAT Number
+shift :: (MonadSAT m) => Number -> m Number
 shift a = do
     false <- Satchmo.Boolean.constant False 
     return $ make $ false : bits a
 
-times1 :: Boolean -> Number -> SAT Number
+times1 :: (MonadSAT m) => Boolean -> Number -> m Number
 times1 x b = do
     zs <- mapM ( \ y -> and [x,y] ) $ bits b
     return $ make zs
 
+
+better_times a b = do
+    kzs <- sequence $ do
+          ( i , x ) <- zip [ 0 .. ] $ bits a
+          ( j , y ) <- zip [ 0 .. ] $ bits b
+          return $ do
+                  z <- and [ x, y ]
+                  return ( i+j , [z] ) 
+    zs <- reduce $ M.elems $ M.fromListWith (++) kzs
+    return $ make zs
+
+
+reduce ( ( x:y:z:ps) : qss ) = do
+    ( r, c ) <- full_adder x y z
+    qss' <- plugin c qss
+    reduce $ ( ps ++ [r] ) : qss' 
+reduce ( ( x:y:[]) : qss ) = do
+    ( r, c ) <- half_adder x y 
+    qss' <- plugin c qss
+    reduce $ [r] : qss' 
+reduce ( ( x:[]) : qss ) = do
+    xs <- reduce qss
+    return $ x : xs
+reduce [] = return []
+
+plugin c [] = do
+    assert [ not c ]
+    return []
+plugin c (qs : qss) = 
+    return ((c:qs) : qss)
diff --git a/Satchmo/Boolean.hs b/Satchmo/Boolean.hs
--- a/Satchmo/Boolean.hs
+++ b/Satchmo/Boolean.hs
@@ -1,14 +1,14 @@
-module Satchmo.Boolean 
+module Satchmo.Boolean
 
-( SAT
+( MonadSAT(..)
 , module Satchmo.Boolean.Data
 , module Satchmo.Boolean.Op
-) 
+)
 
 where
 
 import qualified Prelude
 
-import Satchmo.Internal
+import Satchmo.MonadSAT
 import Satchmo.Boolean.Data
 import Satchmo.Boolean.Op
diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs
--- a/Satchmo/Boolean/Data.hs
+++ b/Satchmo/Boolean/Data.hs
@@ -1,11 +1,11 @@
 {-# language MultiParamTypeClasses #-}
 
-module Satchmo.Boolean.Data 
+module Satchmo.Boolean.Data
 
-( Boolean, Booleans
+( Boolean(Constant), Booleans, encode
 , boolean, exists, forall
 , constant
-, not, assert, monadic
+, not, assert, assertW, monadic
 )
 
 where
@@ -15,8 +15,8 @@
 
 import qualified Satchmo.Code as C
 
-import Satchmo.Data 
-import Satchmo.Internal
+import Satchmo.Data
+import Satchmo.MonadSAT
 
 import Data.Map ( Map )
 import qualified Data.Map as M
@@ -31,6 +31,32 @@
              }
      | Constant { value :: Bool }
 
+{-
+
+-- FIXME: @Pepe: what is the reason for these instances?
+
+instance Eq Boolean where
+  b1@Boolean{}  == b2@Boolean{}  = encode b1 == encode b2
+  b1@Constant{} == b2@Constant{} = value  b1 == value  b2
+  _ == _ = False
+
+instance Ord Boolean where
+  b1@Boolean{}  `compare` b2@Boolean{}  = encode b1 `compare` encode b2
+  b1@Constant{} `compare` b2@Constant{} = value  b1 `compare` value  b2
+  Boolean{} `compare` Constant{} = GT
+  Constant{} `compare` Boolean{} = LT
+
+instance Enum Boolean where
+  fromEnum (Constant True)  = -1
+  fromEnum (Constant False) = 0
+  fromEnum (Boolean (Literal lit) dec) = lit
+
+  toEnum 0    = Constant False
+  toEnum (-1) = Constant True
+  toEnum l    = let x = literal l in Boolean x (asks $ \fm -> fromJust (M.lookup x fm))
+
+-}
+
 type Booleans = [ Boolean ]
 
 isConstant :: Boolean -> Bool
@@ -42,18 +68,21 @@
         Boolean {} -> decode b
         Constant {} -> return $ value b
 
-boolean :: SAT Boolean
+boolean :: MonadSAT m => m Boolean
 boolean = exists
 
-exists :: SAT Boolean
+exists :: MonadSAT m => m Boolean
 exists = do
     x <- fresh
     return $ Boolean 
            { encode = x
-           , decode = asks $ \ fm -> fromJust $ M.lookup x fm
+           , decode = asks $ \ fm -> 
+                      ( positive x == )
+                    $ fromJust
+                    $ M.lookup ( variable x ) fm
            }
 
-forall :: SAT Boolean
+forall :: MonadSAT m => m Boolean
 forall = do
     x <- fresh_forall
     return $ Boolean 
@@ -61,7 +90,7 @@
            , decode = error "Boolean.forall cannot be decoded"
            }
 
-constant :: Bool -> SAT Boolean
+constant :: MonadSAT m => Bool -> m Boolean
 constant v = do
     return $ Constant { value = v } 
 
@@ -73,11 +102,18 @@
       }
     Constant {} -> Constant { value = Prelude.not $ value b }
 
-assert :: [ Boolean ] -> SAT ()
+
+assert :: MonadSAT m => [ Boolean ] -> m ()
 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
+
+assertW :: MonadSAT m => Weight -> [ Boolean ] -> m ()
+assertW w bs = do
+    let ( con, uncon ) = partition isConstant bs
+    let cval = Prelude.or $ map value con
+    when ( Prelude.not cval ) $ emitW w $ clause $ map encode uncon
 
 monadic :: Monad m
         => ( [ a ] -> m b )
diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs
--- a/Satchmo/Boolean/Op.hs
+++ b/Satchmo/Boolean/Op.hs
@@ -1,4 +1,4 @@
-module Satchmo.Boolean.Op 
+module Satchmo.Boolean.Op
 
 ( constant
 , and, or, xor
@@ -11,36 +11,41 @@
 import Prelude hiding ( and, or, not )
 import qualified Prelude
 
-import Satchmo.Internal
+import Satchmo.MonadSAT
 import Satchmo.Code
 import Satchmo.Boolean.Data
 
 import Control.Monad ( foldM )
 
-and :: [ Boolean ] -> SAT Boolean
+and :: MonadSAT m => [ Boolean ] -> m Boolean
+and [] = constant True
+and [x]= return x
 and xs = do
     y <- boolean
-    sequence $ do
+    sequence_ $ do
         x <- xs
         return $ assert [ not y, x ]
     assert $ y : map not xs
     return y
 
-or :: [ Boolean ] -> SAT Boolean
+or :: MonadSAT m => [ Boolean ] -> m Boolean
+or [] = constant False
+or [x]= return x
 or xs = do
     y <- and $ map not xs
     return $ not y
 
-xor :: [ Boolean ] -> SAT Boolean
+xor :: MonadSAT m => [ Boolean ] -> m Boolean
 xor [] = constant False
 xor (x:xs) = foldM xor2 x xs
 
 
 -- | implement the function by giving a full CNF
 -- that determines the outcome
-fun2 :: ( Bool -> Bool -> Bool )
+fun2 :: MonadSAT m => 
+        ( Bool -> Bool -> Bool )
      -> Boolean -> Boolean 
-     -> SAT Boolean
+     -> m Boolean
 fun2 f x y = do
     r <- boolean
     sequence_ $ do
@@ -53,9 +58,10 @@
 
 -- | implement the function by giving a full CNF
 -- that determines the outcome
-fun3 :: ( Bool -> Bool -> Bool -> Bool )
+fun3 :: MonadSAT m => 
+        ( Bool -> Bool -> Bool -> Bool )
      -> Boolean -> Boolean -> Boolean
-     -> SAT Boolean
+     -> m Boolean
 fun3 f x y z = do
     r <- boolean
     sequence_ $ do
@@ -69,11 +75,11 @@
             ]
     return r
 
-xor2 :: Boolean -> Boolean -> SAT Boolean
+xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
 xor2 = fun2 (/=)
 
 -- for historic reasons:
-xor2_orig :: Boolean -> Boolean -> SAT Boolean
+xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean
 xor2_orig x y = do
     a <- and [ x, not y ]
     b <- and [ not x, y ]
diff --git a/Satchmo/Code.hs b/Satchmo/Code.hs
--- a/Satchmo/Code.hs
+++ b/Satchmo/Code.hs
@@ -18,9 +18,9 @@
 import Control.Monad.Reader
 
 
-class Decode c a | c -> a where decode :: c -> Decoder a
+class Decode c a where decode :: c -> Decoder a
 
-type Decoder a = Reader ( Map Literal Bool ) a
+type Decoder a = Reader ( Map Variable Bool ) a
 
 instance Decode () () where
     decode () = return ()
@@ -30,6 +30,10 @@
 
 instance ( Decode c a ) => Decode [c] [a] where
     decode = mapM decode 
+
+instance Decode a b => Decode ( Maybe a ) ( Maybe b ) where
+    decode ( Just b ) = fmap Just $ decode b
+    decode Nothing = return $ Nothing
 
 instance (Ix i, Decode c a) => Decode ( Array i c) ( Array i a ) where
     decode x = do
diff --git a/Satchmo/Counting.hs b/Satchmo/Counting.hs
--- a/Satchmo/Counting.hs
+++ b/Satchmo/Counting.hs
@@ -11,7 +11,7 @@
 
 import Satchmo.Boolean
 
-atleast_block :: Int -> [ Boolean ] -> SAT [ Boolean ]
+atleast_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
 atleast_block k [] = do
     t <- constant True
     f <- constant False
@@ -25,13 +25,13 @@
                      p <- and [ x, cs !! (i-1) ]
                      or [ cs !! i, p ]
 
-atleast :: Int -> [ Boolean ] -> SAT Boolean
+atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
 atleast k xs = do
     cs <- atleast_block k xs
     return $ cs !! k
         
 
-atmost_block :: Int -> [ Boolean ] -> SAT [ Boolean ]
+atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
 atmost_block k [] = do
     t <- constant $ True
     return $ replicate (k+1) t
@@ -45,13 +45,13 @@
             q <- and [ not x, cs !! i ]
             or [ p, q ]
 
-atmost :: Int -> [ Boolean ] -> SAT Boolean
+atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
 atmost k xs = do
     cs <- atmost_block k xs
     return $ cs !! k
         
 
-exactly_block :: Int -> [ Boolean ] -> SAT [ Boolean ]
+exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
 exactly_block k [] = do
     t <- constant True
     f <- constant False
@@ -66,7 +66,7 @@
             q <- and [ not x, cs !! i ]
             or [ p, q ]
 
-exactly :: Int -> [ Boolean ] -> SAT Boolean
+exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
 exactly k xs = do
     cs <- exactly_block k xs
     return $ cs !! k
diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs
--- a/Satchmo/Data.hs
+++ b/Satchmo/Data.hs
@@ -1,15 +1,17 @@
 module Satchmo.Data 
 
 ( CNF, cnf, clauses
-, Clause, clause, literals
-, Literal, literal, nicht
+-- FIXME: exports should be abstract
+, Clause(..), clause, literals
+, Literal(..), literal, nicht
+, Variable, variable, positive
 )
 
 where
 
 import Control.Monad.State.Strict
 
-data CNF     = CNF { clauses :: [ Clause  ] }
+newtype CNF     = CNF { clauses :: [ Clause  ] }
 
 instance Show CNF where
     show ( CNF cs ) = unlines $ map show cs
@@ -18,7 +20,7 @@
 cnf cs = CNF cs
 
 
-data Clause  = Clause { literals :: [ Literal ] }
+newtype Clause  = Clause { literals :: [ Literal ] }
 
 instance Show Clause where
     show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )
@@ -27,16 +29,31 @@
 clause ls = Clause { literals = ls }
 
 
-data Literal = Literal Int 
+newtype Literal = Literal Int
     deriving ( Eq, Ord )
 
 instance Show Literal where 
     show ( Literal i ) = show i
 
-literal :: Int -> Literal
-literal i | i /= 0 = Literal i
+instance Read Literal where
+    readsPrec p = \ cs -> do
+        ( i, cs') <- readsPrec p cs
+        return ( Literal i , cs' )
 
+literal :: Bool -> Variable -> Literal
+literal p v | v /= 0 = 
+    Literal $ if p then v else negate v
 
+
 nicht :: Literal -> Literal
 nicht ( Literal i ) = Literal $ negate i
+
+-- FIXME: should be newtype
+type Variable = Int
+
+variable :: Literal -> Variable
+variable ( Literal v ) = abs v
+
+positive :: Literal -> Bool
+positive ( Literal v ) = 0 < v
 
diff --git a/Satchmo/Integer.hs b/Satchmo/Integer.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Integer.hs
@@ -0,0 +1,10 @@
+module Satchmo.Integer 
+
+( module Satchmo.Integer.Data 
+, module Satchmo.Integer.Op 
+)
+
+where
+
+import Satchmo.Integer.Data
+import Satchmo.Integer.Op
diff --git a/Satchmo/Integer/Data.hs b/Satchmo/Integer/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Integer/Data.hs
@@ -0,0 +1,67 @@
+{-# language MultiParamTypeClasses #-}
+
+module Satchmo.Integer.Data 
+
+( Number, make, number
+, constant
+, bits, width
+)
+
+where
+
+import Prelude hiding ( and, or, not )
+
+import qualified Satchmo.Code as C
+
+import Satchmo.Boolean hiding ( constant )
+import qualified  Satchmo.Boolean as B
+
+import Satchmo.Counting
+
+data Number = Number 
+            { bits :: [ Boolean ] -- ^ lsb first,
+	         -- using two's complement
+            , decode :: C.Decoder Integer
+            }
+
+instance C.Decode Number Integer where
+    decode = decode
+
+width :: Number -> Int
+width n = length $ bits n
+
+-- | declare a number variable (bit width)
+number :: MonadSAT m => Int -> m Number
+number w = do
+    xs <- sequence $ replicate w boolean
+    return $ make xs
+
+make :: [ Boolean ] -> Number
+make xs = Number
+           { bits = xs
+           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys
+           }
+
+fromBinary :: [ Bool ] -> Integer
+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs
+
+toBinary :: Integer -> [ Bool ]
+toBinary 0 = []
+toBinary n  = 
+    let (d,m) = divMod n 2
+    in  toEnum ( fromIntegral m ) : toBinary d
+
+-- | declare a number constant 
+constant :: MonadSAT m 
+	 => Int -- ^ bit width
+	 -> Integer -- ^ value
+	 -> m Number
+constant w n = do
+    xs <- if 0 <= n && n < 2^(w-1)
+          then mapM B.constant $ toBinary n
+	  else if negate ( 2^(w-1)) <= n && n < 0
+	  then mapM B.constant $ toBinary (n + 2^w)
+	  else error "Satchmo.Integer.Data.constant"
+    z <- B.constant False
+    return $ make $ take w $ xs ++ repeat z
+
diff --git a/Satchmo/Integer/Op.hs b/Satchmo/Integer/Op.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Integer/Op.hs
@@ -0,0 +1,129 @@
+-- | all operations have fixed bit length,
+-- and are unsatisfiable in case of overflows.
+
+module Satchmo.Integer.Op 
+
+( negate, add, sub, times
+, gt, ge, eq 
+)
+
+where
+
+import Satchmo.Integer.Data
+import Prelude hiding ( and, or, not, negate )
+import Satchmo.Boolean hiding ( constant )
+import qualified  Satchmo.Boolean as B
+
+import qualified Satchmo.Binary.Op.Common as C
+import qualified Satchmo.Binary.Op.Flexible as F
+
+import Control.Monad ( forM, when )
+
+-- | negate. Unsatisfiable if value is lowest negatve.
+negate :: MonadSAT m 
+       => Number -> m Number
+negate n = do
+    let ys = map B.not $ bits n 
+    o <- B.constant True
+    ( zs, c ) <- increment ys o
+    assert [ last $ ys, B.not $ last zs ]
+    return $ make zs
+
+increment [] z = return ( [], z )
+increment (y:ys) z = do
+    ( r, d ) <- C.half_adder y z
+    ( rs, c ) <- increment ys d
+    return ( r : rs, c )
+
+add :: MonadSAT m 
+    => Number -> Number 
+    -> m Number
+add a b = do
+    when ( width a /= width b ) 
+    	 $ error "Satchmo.Integer.Op.add"
+    cin <- B.constant False
+    ( zs, cout ) <- 
+        F.add_with_carry cin ( bits a ) ( bits b )
+    monadic assert [ fun2 (==) cout $ last zs ]
+    return $ make zs
+
+sub :: MonadSAT m 
+    => Number -> Number 
+    -> m Number
+sub a b = do
+    when ( width a /= width b ) 
+    	 $ error "Satchmo.Integer.Op.sub"
+    c <- negate b
+    add a c
+
+times :: MonadSAT m 
+    => Number -> Number 
+    -> m Number
+times a b = do
+    when ( width a /= width b ) 
+    	 $ error "Satchmo.Integer.Op.times"
+    c <- F.times ( F.make $ bits a ) 
+      	 	 ( F.make $ bits b )
+    let ( pre, post ) = splitAt ( width a ) $ F.bits c
+    monadic assert [ fun2 (==) ( head post) $ last pre ]
+    return $ make pre
+
+----------------------------------------------------
+
+positive :: MonadSAT m
+	 => Number 
+	 -> m Boolean
+positive n = do
+    ok <- or $ init $ bits n   
+    and [ ok, not $ last $ bits n ]
+
+negative :: MonadSAT m
+	 => Number 
+	 -> m Boolean
+negative n = do
+    return $ last $ bits n
+
+nonnegative :: MonadSAT m
+	 => Number 
+	 -> m Boolean
+nonnegative n = do
+    return $ not $ last $ bits n
+
+----------------------------------------------------
+
+eq :: MonadSAT m 
+   => Number -> Number
+   -> m Boolean
+eq a b = do
+    when ( width a /= width b ) 
+    	 $ error "Satchmo.Integer.Op.eq"
+    eqs <- forM ( zip ( bits a ) ( bits b ) )
+    	   $ \ (x,y) -> fun2 (==) x y
+    and eqs
+
+gt :: MonadSAT m 
+   => Number -> Number
+   -> m Boolean
+gt a b = do
+    diff <- and [ not $ last $ bits a, last $ bits b ]
+    same <- fun2 (==) ( last $ bits a )	
+     	     	       ( last $ bits b )
+    g <- F.gt ( F.make $ bits a ) 
+      	      ( F.make $ bits b )
+    monadic or [ return diff
+    	       , and [ same, g ]
+	       ]
+
+ge :: MonadSAT m 
+   => Number -> Number
+   -> m Boolean
+ge a b = do
+    diff <- and [ not $ last $ bits a, last $ bits b ]
+    same <- fun2 (==) ( last $ bits a )	
+     	     	       ( last $ bits b )
+    g <- F.ge ( F.make $ bits a ) 
+      	      ( F.make $ bits b )
+    monadic or [ return diff
+    	       , and [ same, g ]
+	       ]
+    
diff --git a/Satchmo/Internal.hs b/Satchmo/Internal.hs
deleted file mode 100644
--- a/Satchmo/Internal.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-module Satchmo.Internal 
-
-( SAT
-, fresh, fresh_forall
-, emit
-, sat
-)
-
-where
-
-import Satchmo.Data
-
-import Control.Monad.State.Strict
-import Control.Monad.Writer.Strict
-
-data Quantified = Forall [ Int ] | Exists [ Int ]
-
-data Accu = Accu 
-          { next :: ! Int
-          , quantified :: [ Quantified ]
-          , size :: ! Int
-          }
-
-start :: Accu
-start = Accu 
-      { next = 1
-      , quantified = []
-      , size = 0
-      }
-
-type SAT a = WriterT [ Clause ] (State Accu) a
-
-sat :: SAT a -> ( String, a )
-sat m = 
-    let ~( ~(a,w), accu) = runState ( runWriterT m ) start
-    in  ( unlines $ unwords [ "p", "cnf", show ( next accu - 1), show ( size accu ) ]
-                  : do q <- reverse $ interesting $ quantified accu
-                       return $ case q of 
-                           Forall xs -> unwords $ "a" : map show ( reverse xs ++ [0] )
-                           Exists xs -> unwords $ "e" : map show ( reverse xs ++ [0] )
-                  ++ map show w
-        , a
-        )
-    
-interesting [ Exists _ ] = []
-interesting xs = xs
-
--- | existentially quantified (implicitely so, before first fresh_forall)
-fresh :: SAT Literal
-fresh = do
-    a <- get
-    let n = next a
-    let q = case quantified a of
-              Exists xs : rest -> Exists (n : xs) : rest
-              rest -> Exists [n] : rest
-    put $ a { next = n + 1, quantified = q }
-    return $ literal n
-
--- | universally quantified
-fresh_forall :: SAT Literal
-fresh_forall = do
-    a <- get
-    let n = next a
-    let q = case quantified a of
-              Forall xs : rest -> Forall (n : xs) : rest
-              rest -> Forall [n] : rest
-    put $ a { next = n + 1, quantified = q }
-    return $ literal n
-
-emit :: Clause -> SAT ()
-emit clause = do
-    a <- get
-    tell [ clause ]
-    put $ a 
-        { size = size a + 1 
-        }
-
-
diff --git a/Satchmo/MonadSAT.hs b/Satchmo/MonadSAT.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/MonadSAT.hs
@@ -0,0 +1,90 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Satchmo.MonadSAT
+
+( MonadSAT(..), Weight
+)
+
+where
+
+import Satchmo.Data
+
+import Control.Monad.Trans (lift)
+import Control.Monad.Cont  (ContT)
+import Control.Monad.List  (ListT)
+import Control.Monad.Reader (ReaderT)
+import qualified Control.Monad.State  as Lazy (StateT)
+import qualified Control.Monad.Writer as Lazy (WriterT)
+import qualified Control.Monad.RWS    as Lazy (RWST)
+import qualified Control.Monad.State.Strict  as Strict (StateT)
+import qualified Control.Monad.Writer.Strict as Strict (WriterT)
+import qualified Control.Monad.RWS.Strict    as Strict (RWST)
+import Data.Monoid
+
+type Weight = Int
+
+class (Functor m, Monad m) => MonadSAT m where
+  fresh, fresh_forall :: m Literal
+  emit  :: Clause -> m ()
+  emitW :: Weight -> Clause -> m ()
+
+
+-- -------------------------------------------------------
+-- MonadSAT liftings for standard monad transformers
+-- -------------------------------------------------------
+
+instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
+
+instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where
+  fresh = lift fresh
+  fresh_forall = lift fresh_forall
+  emit  = lift . emit
+  emitW = (lift.) . emitW
diff --git a/Satchmo/Polynomial.hs b/Satchmo/Polynomial.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Polynomial.hs
@@ -0,0 +1,137 @@
+{-# language MultiParamTypeClasses #-}
+{-# language FlexibleContexts      #-}
+{-# language UndecidableInstances  #-}
+
+module Satchmo.Polynomial 
+
+( Number ()
+, number, constant
+, iszero, equals, ge, gt
+, add, times
+)
+
+where
+
+import Data.Map ( Map )
+import qualified Data.Map as M
+
+import Satchmo.SAT
+import Satchmo.Boolean hiding ( constant )
+import qualified Satchmo.Boolean 
+import Satchmo.Code
+
+import qualified Satchmo.Binary.Op.Fixed as F
+
+import Control.Monad ( forM )
+
+-- | polynomial in one variable,
+-- coefficients starting from degree zero
+data Poly a = Poly [a] deriving ( Eq, Ord, Show )
+
+type Number = Poly F.Number
+
+-- Hohoho:
+instance Decode a Integer => Decode ( Poly a ) Integer where
+    decode ( Poly xs ) = do
+        ys <- forM xs decode 
+        let base = 1000 -- well
+        return $ if all ( < base ) ys
+                 then foldr ( \ y o -> o * base + y ) 0 ys
+                 else error "Satchmo.Polynomial.decode"
+
+-- | this is sort of wrong:
+-- null polynomial should have degree -infty
+-- but this function will return -1
+degree :: Poly a -> Int
+degree ( Poly xs ) = pred $ length xs
+
+
+number :: MonadSAT m
+       => Int -- ^ bits
+       -> Int -- ^ degree
+       -> m ( Poly F.Number )
+number bits deg = do 
+    xs <- forM [ 0 .. deg ] $ \ i -> F.number bits
+    return $ Poly xs
+
+constant :: MonadSAT m
+         => Integer
+         -> m ( Poly F.Number )
+constant 0 = return $ Poly []
+constant c = do
+    z <- F.constant 0
+    o <- F.constant c
+    return $ Poly [ z, o ]
+
+iszero  ( Poly xs ) = do
+    ns <- forM xs $ F.iszero
+    Satchmo.Boolean.and ns
+
+equals ( Poly xs ) ( Poly ys ) = do
+          z <- F.constant 0
+          let n = max ( length xs ) ( length ys )
+              fill xs = take n $ xs ++ repeat z
+          let handle xs ys = case ( xs, ys ) of
+                  ( [], [] ) -> Satchmo.Boolean.constant True
+                  (x:xs, y:ys) -> do
+                      e <- F.equals x y
+                      later <- handle xs ys
+                      Satchmo.Boolean.and [ e, later ]
+          handle ( reverse $ fill xs ) ( reverse $ fill ys )
+
+ge ( Poly xs ) ( Poly ys ) = do
+          z <- F.constant 0
+          let n = max ( length xs ) ( length ys )
+              fill xs = take n $ xs ++ repeat z
+          let handle xs ys = case ( xs, ys ) of
+                  ( [], [] ) -> Satchmo.Boolean.constant True
+                  (x:xs, y:ys) -> do
+                      gt <- F.gt x y
+                      e <- F.equals x y
+                      later <- handle xs ys
+                      monadic Satchmo.Boolean.or 
+                              [ return gt
+                              , Satchmo.Boolean.and [ e, later ]
+                              ]
+          handle ( reverse $ fill xs ) ( reverse $ fill ys )
+
+gt  ( Poly xs ) ( Poly ys ) = do
+          z <- F.constant 0
+          let n = max ( length xs ) ( length ys )
+              fill xs = take n $ xs ++ repeat z
+          let handle xs ys = case ( xs, ys ) of
+                  ( [], [] ) -> Satchmo.Boolean.constant False
+                  (x:xs, y:ys) -> do
+                      gt <- F.gt x y
+                      e <- F.equals x y
+                      later <- handle xs ys
+                      monadic Satchmo.Boolean.or 
+                              [ return gt
+                              , Satchmo.Boolean.and [ e, later ]
+                              ]
+          handle ( reverse $ fill xs ) ( reverse $ fill ys )
+
+
+add ( Poly xs ) ( Poly ys ) = do
+          let handle xs ys = case ( xs, ys ) of
+                  ( [] , ys ) ->  return ys
+                  ( xs, [] ) -> return xs
+                  (x:xs, y:ys) -> do
+                      z <- F.add x y
+                      zs <- handle xs ys
+                      return $ z : zs
+          zs <- handle xs ys
+          return $ Poly zs
+
+times p q = do
+          let handle ( Poly xs ) ( Poly ys ) = 
+                  case ( xs, ys ) of
+                      ( [], ys ) -> return $ Poly []
+                      ( xs, [] ) -> return $ Poly []
+                      ( x : xs, ys ) -> do
+                          Poly zs <- handle ( Poly xs ) ( Poly ys )
+                          f : fs  <- forM ys $ F.times x
+                          Poly rest <- add ( Poly zs ) ( Poly fs )
+                          return $ Poly $ f : rest
+          handle p q
+
diff --git a/Satchmo/Relation/Data.hs b/Satchmo/Relation/Data.hs
--- a/Satchmo/Relation/Data.hs
+++ b/Satchmo/Relation/Data.hs
@@ -3,7 +3,7 @@
 module Satchmo.Relation.Data
 
 ( Relation, relation, build
-, bounds, (!), indices
+, bounds, (!), indices, assocs
 , table
 ) 
 
@@ -13,14 +13,14 @@
 import Satchmo.Boolean
 
 import qualified Data.Array as A
-import Data.Array hiding ( bounds, (!), indices )
+import Data.Array hiding ( bounds, (!), indices, assocs )
 
 import Control.Monad ( guard )
 
 data Relation a b = Relation ( Array (a,b) Boolean ) 
 
-relation :: ( Ix a, Ix b ) 
-         => ((a,b),(a,b)) -> SAT ( Relation a b ) 
+relation :: ( Ix a, Ix b, MonadSAT m ) 
+         => ((a,b),(a,b)) -> m ( Relation a b ) 
 relation bnd = do
     pairs <- sequence $ do 
         p <- range bnd
@@ -39,6 +39,9 @@
 bounds ( Relation r ) = A.bounds r
 
 indices ( Relation r ) = A.indices r
+
+assocs ( Relation r ) = A.assocs r
+
 
 Relation r ! p = r A.! p
 
diff --git a/Satchmo/Relation/Op.hs b/Satchmo/Relation/Op.hs
--- a/Satchmo/Relation/Op.hs
+++ b/Satchmo/Relation/Op.hs
@@ -6,6 +6,7 @@
 , union
 , complement
 , product
+, intersection
 ) 
 
 where
@@ -30,17 +31,17 @@
 complement r = 
     build (bounds r) $ do i <- indices r ; return ( i, not $ r!i )
 
-union :: ( Ix a , Ix b ) 
+union :: ( Ix a , Ix b, MonadSAT m ) 
       => Relation a b -> Relation a b 
-      -> SAT ( Relation a b )
+      -> m ( Relation a b )
 union r s = do
     pairs <- sequence $ do
         i <- indices r
         return $ do o <- or [ r!i, s!i ] ; return ( i, o )
     return $ build ( bounds r ) pairs
 
-product :: ( Ix a , Ix b, Enum b, Ix c ) 
-        => Relation a b -> Relation b c -> SAT ( Relation a c )
+product :: ( Ix a , Ix b, Ix c, MonadSAT m ) 
+        => Relation a b -> Relation b c -> m ( Relation a c )
 product a b = do
     let ((ao,al),(au,ar)) = bounds a
         ((bo,bl),(bu,br)) = bounds b
@@ -49,9 +50,18 @@
         i @ (x,z) <- range bnd
         return $ do
             o <- monadic or $ do
-                y <- [ al .. ar ]
+                y <- range ( al, ar )
                 return $ and [ a!(x,y), b!(y,z) ]
             return ( i, o )
     return $ build bnd pairs
+
+intersection :: ( Ix a , Ix b, MonadSAT m ) 
+      => Relation a b -> Relation a b 
+      -> m ( Relation a b )
+intersection r s = do
+    pairs <- sequence $ do
+        i <- indices r
+        return $ do a <- and [ r!i, s!i ] ; return ( i, a )
+    return $ build ( bounds r ) pairs
 
 
diff --git a/Satchmo/Relation/Prop.hs b/Satchmo/Relation/Prop.hs
--- a/Satchmo/Relation/Prop.hs
+++ b/Satchmo/Relation/Prop.hs
@@ -4,6 +4,7 @@
 , symmetric 
 , transitive
 , irreflexive
+, reflexive
 , regular
 )
 
@@ -21,31 +22,38 @@
 import Control.Monad ( guard )
 import Data.Ix
 
-implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean
+implies :: ( Ix a, Ix b, MonadSAT m ) 
+        => Relation a b -> Relation a b -> m Boolean
 implies r s = monadic and $ do
     i <- indices r
     return $ or [ not $ r ! i, s ! i ]
 
 
-symmetric :: (Enum a, Ix a) => Relation a a -> SAT Boolean
+symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
 symmetric r = implies r ( mirror r )
 
-irreflexive :: (Enum a, Ix a) => Relation a a -> SAT Boolean
+irreflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean
 irreflexive r = and $ do
     let ((a,b),(c,d)) = bounds r
-    x <- [a .. c]
+    x <- range ( a, c)
     return $ Satchmo.Boolean.not $ r ! (x,x) 
 
-regular :: (Enum a, Ix a) => Int -> Relation a a -> SAT Boolean
+reflexive :: ( Ix a, MonadSAT m) => Relation a a -> m 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
 regular deg r = monadic and $ do
     let ((a,b),(c,d)) = bounds r
-    x <- [ a .. c ]
+    x <- range ( a , c )
     return $ exactly deg $ do 
-        y <- [ b .. d ]
+        y <- range (b,d)
         return $ r !(x,y)
 
-transitive :: ( Enum a, Ix a ) 
-           => Relation a a -> SAT Boolean
+transitive :: ( Ix a, MonadSAT m ) 
+           => Relation a a -> m Boolean
 transitive r = do
     r2 <- product r r
     implies r2 r
diff --git a/Satchmo/SAT.hs b/Satchmo/SAT.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT.hs
@@ -0,0 +1,101 @@
+{-# 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}
+
diff --git a/Satchmo/SAT/Weighted.hs b/Satchmo/SAT/Weighted.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/Weighted.hs
@@ -0,0 +1,88 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+module Satchmo.SAT.Weighted (SAT, sat, MaxWeight, Header(..)) where
+
+import Satchmo.Data
+import Satchmo.MonadSAT
+
+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 System.Directory
+import System.Environment
+import System.IO
+
+
+instance MonadSAT SAT where
+  fresh = satfresh
+  fresh_forall = satfresh_forall
+  emit  = satemit Nothing
+  emitW = satemit . Just
+
+-- ---------------
+-- Implementation
+-- ---------------
+
+data Accu = Accu
+          { next :: ! Int
+          , universal :: [Int]
+          , size :: ! Int
+          }
+
+start :: Accu
+start = Accu
+      { next = 1
+      , universal = []
+      , size = 0
+      }
+
+type MaxWeight  = Int
+
+newtype SAT a = SAT {unsat::RWST (Handle, MaxWeight) () Accu IO a}
+    deriving (MonadState Accu, MonadReader (Handle, MaxWeight), Monad, MonadIO, Functor)
+
+data Header = Header { numClauses, numVars, maxWeight :: Int
+                     , universals :: [Int]
+                     }
+
+sat :: MaxWeight -> SAT a -> IO (BS.ByteString, Header, a )
+sat maxW (SAT m) =
+ bracket
+    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))
+    (\(fp, h) -> removeFile fp)
+    (\(fp, h) -> do
+       hSetBuffering h (BlockBuffering Nothing)
+       ~(a, accu, _) <- runRWST m (h, maxW) start
+       hClose h
+       let header = Header (size accu) (next accu - 1) maxW 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 :: Maybe Weight -> Clause -> SAT ()
+satemit w (Clause clause) = do
+    a <- get
+    (h,maxW) <- ask
+    liftIO $ BS.hPut h (bshowClause $ Clause(Literal (fromMaybe maxW w) : clause))
+    put $ a { size = size a + 1}
+
+  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
+
diff --git a/Satchmo/Simple.hs b/Satchmo/Simple.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Simple.hs
@@ -0,0 +1,30 @@
+{-# language GeneralizedNewtypeDeriving #-}
+
+module Satchmo.Simple where
+
+import Satchmo.MonadSAT
+import Satchmo.Data
+
+import Control.Monad.State
+
+data Accu = Accu { next :: ! Int
+                 , pool :: [ Clause ]
+                 }
+
+start = Accu { next = 0, pool = [] }
+
+sat (SAT m) = flip evalState start
+            $ do x <- m; a <- get ; return (cnf $ pool a, x) 
+
+newtype SAT a = SAT { unsat :: State Accu a } 
+    deriving ( Functor, Monad )
+
+instance MonadSAT SAT where
+    fresh = SAT $ do 
+          a <- get ; let n = succ $ next a 
+          put $ a { next = n } ; return $ Literal n
+    emit c = SAT $ do
+          modify $ \ a -> a { pool = c : pool a }
+
+
+        
diff --git a/Satchmo/Solve.hs b/Satchmo/Solve.hs
--- a/Satchmo/Solve.hs
+++ b/Satchmo/Solve.hs
@@ -3,8 +3,8 @@
 
 module Satchmo.Solve
 
-( solve
-, Implementation
+( solve, solveW
+, Implementation, WeightedImplementation
 , Decoder
 )
 
@@ -12,28 +12,50 @@
 
 import Satchmo.Data
 import Satchmo.Code
-import Satchmo.Internal
+import Satchmo.SAT
+import qualified Satchmo.SAT.Weighted as Weighted
 
+import qualified Data.ByteString.Lazy.Char8 as BS
 import Data.Map ( Map )
 import qualified Data.Map as M
 
-import Control.Monad.State
 import Control.Monad.Reader
 
-type Implementation = String -> IO ( Maybe ( Map Literal Bool ) )
+import System.IO
 
-solve :: Implementation
-      -> SAT ( Decoder a )
-    -> IO ( Maybe a )
+type Implementation = BS.ByteString 
+                    -> Header 
+                    -> IO ( Maybe ( Map Variable Bool ) )
+
+type WeightedImplementation = BS.ByteString 
+                            -> Weighted.Header 
+                            -> IO ( Maybe ( Map Variable Bool ) )
+
+solve :: Implementation 
+      -> SAT ( Decoder a ) 
+      -> IO ( Maybe a )
 solve implementation build = do
-    let (s, a) = sat build
-    mfm <- implementation s
+    (s, h, a) <- sat build
+    mfm <- implementation s h
     case mfm of
         Nothing -> do
-            putStrLn "not satisfiable"
+            hPutStrLn stderr "not satisfiable"
             return Nothing
         Just fm -> do
-            putStrLn "satisfiable"
-            -- print fm
+            hPutStrLn stderr "satisfiable"
             return $ Just $ runReader a fm
-                
+
+solveW :: Weighted.MaxWeight 
+       -> WeightedImplementation 
+       -> Weighted.SAT (Decoder a) 
+       -> IO (Maybe a)
+solveW maxW implementation build = do
+    (s, h, a) <- Weighted.sat maxW build
+    mfm <- implementation s h
+    case mfm of
+        Nothing -> do
+            hPutStrLn stderr "not satisfiable"
+            return Nothing
+        Just fm -> do
+            hPutStrLn stderr "satisfiable"
+            return $ Just $ runReader a fm
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,17 +1,19 @@
 Name:           satchmo
-Version:        1.4
+Version:        1.8.0
 
 License:        GPL
 License-file:	gpl-2.0.txt
-Author:         Johannes Waldmann
+Author:         Pepe Iborra, Johannes Waldmann
 Maintainer:	Johannes Waldmann
 Homepage:       http://dfa.imn.htwk-leipzig.de/satchmo/
+		http://github.com/pepeiborra/satchmo/
 Synopsis:       SAT encoding monad
 description:	Encoding for boolean and integral constraints into (QBF-)CNF-SAT.
 		The encoder is provided as a State monad (hence the "mo" in "satchmo").
-		requires a backend (e.g. satchmo-backends, satchmo-funsat)
+		This package contains functions that construct problems,
+                to solve them, you need package satchmo-backends.
 Category:	Algorithms
-Build-depends:  mtl, process, containers, base, array
+Build-depends:  mtl, process, containers, base >= 3 && <= 4, array, bytestring, directory
 Exposed-modules:
 	Satchmo.Data
         Satchmo.Solve
@@ -19,18 +21,27 @@
 	Satchmo.Counting
 	Satchmo.Code
 	Satchmo.Binary
+	Satchmo.Integer
 	Satchmo.Binary.Op.Common
 	Satchmo.Binary.Op.Fixed
 	Satchmo.Binary.Op.Flexible
+	Satchmo.Polynomial
 	Satchmo.Relation
 	Satchmo.Relation.Data
 	Satchmo.Relation.Op
 	Satchmo.Relation.Prop
+	Satchmo.MonadSAT
+	Satchmo.SAT
+	Satchmo.Simple
+	Satchmo.SAT.Weighted
 Other-modules:
 	Satchmo.Binary.Data
+	Satchmo.Integer.Data
         Satchmo.Boolean.Op
+        Satchmo.Integer.Op
         Satchmo.Boolean.Data
-	Satchmo.Internal
 hs-source-dirs:	.
 extensions: 
 build-type: Simple
+ghc-options: -funbox-strict-fields
+ghc-prof-options: -auto