diff --git a/Satchmo/Solver/Clasp.hs b/Satchmo/Solver/Clasp.hs
deleted file mode 100644
--- a/Satchmo/Solver/Clasp.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# language PatternSignatures #-}
-
--- | http://www.cs.uni-potsdam.de/clasp/
-
-module Satchmo.Solver.Clasp
-
-( solve
-, using
-)
-
-where
-
-import Satchmo.Data
-import Satchmo.SAT
-import qualified Satchmo.Solve
-import Satchmo.Solver.Internal
-
-import Data.Monoid
-import System.Process
-import System.Exit
-import System.IO
-import Control.Monad ( when )
-import Control.Concurrent
-import Control.Exception
-
-import qualified Data.ByteString.Char8 as S
-import qualified Data.ByteString.Lazy.Char8 as BS
--- import qualified Data.ByteString.Lazy as BS
-
-import qualified Data.Map as M
-
-solve = using "clasp"
-
-using fp = Satchmo.Solve.solve $ clasp fp
-
-clasp :: FilePath -> Satchmo.Solve.Implementation
-clasp fp cs Header{numVars=numVars, numClauses=numClauses}   = do
-    let header = mkDimacsHeader numVars numClauses
-        cs'    = BS.pack ( header ++ "\n" ) `mappend` cs
-    let debug = False
-    if debug 
-       then BS.hPut stderr cs'
-       else hPutStrLn stderr header 
-
-    ( hin, hout, herr, proc ) <- 
-        System.Process.runInteractiveCommand
-            $ unwords [ fp, "--dimacs",  "--number=1",  "--sat-p=20,25,150"
-                      , "--hParam=0,512"  ] 
-
-    container <- newEmptyMVar
-    forkIO $ do 
-        -- hPutStrLn stderr "before hPut"
-        BS.hPut hin cs'
-        -- waitForProcess proc
-        -- hPutStrLn stderr "before hGetContents"
-        ds <- hGetContents hout
-        hPutStrLn stderr $ unwords [ "output", "length", show ( length ds ) ]
-        putMVar container ds
-
-    out <- takeMVar container 
-        `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
-            -- hPutStrLn stderr "caught exception"
-            terminateProcess proc
-            return ""
-
-    when debug $ hPutStrLn stdout out
-    let 
-        assign = M.fromList $ do
-                'v' : xs <- lines out
-                l <- map read $ takeWhile ( /= "0" ) $ words xs
-                return ( variable l, positive l )
-        status = filter ( \ cs -> take 1 cs == "s" ) $ lines out
-    case status of
-        "s SATISFIABLE" : post  -> do
-            return $ Just assign
-        _ -> do
-            return $ Nothing
-
diff --git a/Satchmo/Solver/Internal.hs b/Satchmo/Solver/Internal.hs
--- a/Satchmo/Solver/Internal.hs
+++ b/Satchmo/Solver/Internal.hs
@@ -10,10 +10,19 @@
         (hIn, hOut, hErr, hProc) <- 
             runInteractiveProcess exec args Nothing Nothing
         try (BS.hPut hIn input) :: IO (Either AsyncException ())
+        stdout <- BS.hGetContents hOut
+        stderr <- hGetContents hErr
+        code   <- waitForProcess hProc
+        return (code, BS.unpack stdout, stderr)
+
+readProcessWithExitCodeS exec args input = do
+        (hIn, hOut, hErr, hProc) <- 
+            runInteractiveProcess exec args Nothing Nothing
+        try (S.hPut hIn input) :: IO (Either AsyncException ())
         stdout <- S.hGetContents hOut
         stderr <- hGetContents hErr
         code   <- waitForProcess hProc
         return (code, S.unpack stdout, stderr)
 
 mkDimacsHeader numVars numClauses = 
-    "p cnf " ++ show numVars ++ " " ++ show numClauses 
+    "p cnf " ++ show numVars ++ " " ++ show numClauses ++ "\n"
diff --git a/Satchmo/Solver/Minisat.hs b/Satchmo/Solver/Minisat.hs
--- a/Satchmo/Solver/Minisat.hs
+++ b/Satchmo/Solver/Minisat.hs
@@ -11,75 +11,70 @@
 import Satchmo.Data
 import qualified Satchmo.Solve
 import Satchmo.Solver.Internal
-import Satchmo.SAT
+import Satchmo.SAT.Seq
 
-import qualified Data.ByteString.Char8 as S
-import qualified Data.ByteString.Lazy.Char8 as BS
--- import qualified Data.ByteString.Lazy as BS
+import qualified Data.ByteString.Char8 as BS
+-- import qualified Data.ByteString.Lazy.Char8 as BS
 
 import Data.Monoid
-import System.IO (stderr, hFlush, hClose, hPutStrLn, hGetContents
-       , hSetBuffering, BufferMode (..) )
+import System.IO 
 import System.Process
 import Control.Monad ( when )
 import Control.Concurrent
 import Control.Exception
-import qualified Control.Exception as C
 
-import qualified Data.Map as M
+import System.TimeIt
+import Text.Printf
 
-solve = using "/usr/bin/minisat2"
+-- import qualified Data.Map as M
+import qualified Data.Array as A
 
+solve = using "minisat2"
+
 using fp = Satchmo.Solve.solve $ minisat fp
 
 minisat :: FilePath -> Satchmo.Solve.Implementation
 minisat fp cs Header{numVars=numVars, numClauses=numClauses} = do
-    let header = mkDimacsHeader numVars numClauses
-        cs'    = BS.pack header `mappend` cs
+    let header = BS.pack $ mkDimacsHeader numVars numClauses
+    
     let debug = False
-    if debug
-       then BS.hPut stderr cs'
-       else hPutStrLn stderr header >> hFlush stderr
-
--- copied from
--- http://hackage.haskell.org/packages/archive/process/1.0.1.5/doc/html/src/System-Process.html#readProcessWithExitCode
-
-    ( Just inh, Just outh, Just errh, pid ) <- 
-       createProcess ( proc fp  [ "/dev/stdin", "/dev/stdout" ] )
-           { std_in  = CreatePipe, std_out = CreatePipe, std_err = CreatePipe }
-
-    outMVar <- newEmptyMVar
-
-    -- fork off a thread to start consuming stdout
-    out  <- hGetContents outh
-    _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
-
-    -- fork off a thread to start consuming stderr
-    err  <- hGetContents errh
-    _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
-
-    -- now write and flush any input
-    do BS.hPut  inh cs'; hFlush inh ; hClose inh -- done with stdin
+    when debug $ do
+        BS.hPutStrLn stderr header
+        BS.hPutStrLn stderr cs
 
-    -- wait on the output
-    takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
-        terminateProcess pid
-    takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
-        terminateProcess pid
-    hClose outh ; hClose errh
+    ( hin, hout, herr, proc ) <- runInteractiveCommand
+           ( unwords [ fp, "/dev/stdin", "/dev/stdout" ] )
+    
+    container <- newEmptyMVar
 
-    -- wait on the process
-    ex <- waitForProcess pid
+    streamer <- forkIO $ do
+        BS.hPutStr hin ( mappend header cs )
+        -- waitForProcess proc
+        ds <- hGetContents hout
+        hPutStrLn stderr $ unwords [ "output", "length", show (length ds) ]
+        hPutStrLn stderr $ take 80 ds
+        putMVar container ds
 
-    hPutStrLn stderr $ unwords [ "output", "length", show ( length out ) ]
-    -- hPutStrLn stderr out
+    out <- takeMVar container `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
+        -- hPutStrLn stderr "got exception in waitForProcess"
+        killThread streamer
+        terminateProcess proc
+        -- hPutStrLn stderr "terminateProcess done"
+        return ""
+    -- hPutStrLn stderr "end waitForProcess"
 
     case lines out of
         "SAT" : xs : _ -> do
-           let dict = Just $ M.fromList $ do
-                            l <- map read $ takeWhile ( /= "0" ) $ words xs
-                            return ( variable l, positive l )
-           when debug $ print dict
-           return dict
+           let dict = Just $ A.listArray (1,numVars) $ do
+                            (v,l) <- zip [1..] $ map read $ takeWhile ( /= "0" ) $ words xs
+                            return $ if variable l == v then  positive l else error "huh"
+           seq (length out) $ return dict
         _ -> return $ Nothing
 
+
+timeItMsg msg action = do 
+    (time, res) <- timeItT action
+    hPrintf stderr "CPU time: %6.2fs for %s\n" time msg    
+    hFlush stderr 
+    return res
+    
diff --git a/Satchmo/Solver/Pcosat.hs b/Satchmo/Solver/Pcosat.hs
--- a/Satchmo/Solver/Pcosat.hs
+++ b/Satchmo/Solver/Pcosat.hs
@@ -24,11 +24,11 @@
 import Control.Concurrent
 import Control.Exception
 
-import qualified Data.ByteString.Char8 as S
-import qualified Data.ByteString.Lazy.Char8 as BS
--- import qualified Data.ByteString.Lazy as BS
+-- import qualified Data.ByteString.Lazy.Char8 as BS
+import qualified Data.ByteString.Char8 as BS
 
-import qualified Data.Map as M
+-- import qualified Data.Map as M
+import qualified Data.Array as A
 
 solve = using "precosat"
 
@@ -40,7 +40,7 @@
 pcosat :: FilePath -> Satchmo.Solve.Implementation
 pcosat fp cs Header{numVars=numVars, numClauses=numClauses}   = do
     let header = mkDimacsHeader numVars numClauses
-        cs'    = BS.pack ( header ++ "\n" ) `mappend` cs
+        cs'    = BS.pack header `mappend` cs
     if debug 
        then BS.hPut stderr cs'
        else hPutStrLn stderr header 
@@ -67,10 +67,20 @@
 
     when debug $ hPutStrLn stdout out
     let core = filter ( \ cs -> take 1 cs /= "c" ) $ lines out
+
+{-
         assign = M.fromList $ do
                 'v' : xs <- core
                 l <- map read $ takeWhile ( /= "0" ) $ words xs
                 return ( variable l, positive l )
+-}
+
+        assign = A.array (1, numVars) $ do
+                'v' : xs <- core
+                l <- map read $ takeWhile ( /= "0" ) $ words xs
+                return ( variable l, positive l )
+            
+
         status = filter ( \ cs -> take 1 cs == "s" ) $ lines out
     case status of
         "s SATISFIABLE" : post  -> do
diff --git a/Satchmo/Solver/Quantor.hs b/Satchmo/Solver/Quantor.hs
deleted file mode 100644
--- a/Satchmo/Solver/Quantor.hs
+++ /dev/null
@@ -1,43 +0,0 @@
-module Satchmo.Solver.Quantor
-
-( solve
-)
-
-where
-
-import Satchmo.Data
-import qualified Satchmo.Solve
-import Satchmo.Solver.Internal
-import Satchmo.SAT
-
-import Data.Monoid
-import qualified Data.ByteString.Char8 as S
-import qualified Data.ByteString.Lazy.Char8 as BS
-import System.IO  (stderr, hFlush, hPutStrLn)
-import System.Process
-import Control.Monad ( when )
-
-import qualified Data.Map as M
-
-solve = Satchmo.Solve.solve quantor
-
-quantor :: Satchmo.Solve.Implementation
-quantor cs Header{numVars=numVars, numClauses=numClauses} = do
-    let header = mkDimacsHeader numVars numClauses
-        cs'    = BS.pack header `mappend` cs
-    let debug = True
-    if debug 
-       then BS.hPut stderr cs'
-       else hPutStrLn stderr header >> hFlush stderr
-    ( code, stdout, stderr ) <- 
-        readProcessWithExitCodeBS "quantor" [ "-v", "--resolve-exported=0" ] cs'
-    when debug $ hPutStrLn System.IO.stderr stdout
-    let 
-    case filter ( \ ws -> take 1 ws /= [ "c" ] ) $ map words $ lines stdout of
-        [ "s", ok ] : rest | ok `elem` [ "TRUE", "SATISFIABLE" ] -> 
-            return $ Just $ M.fromList $ do
-                "v" : vars <- rest
-                l <- map read $ takeWhile ( /= "0" ) vars
-                return ( variable l, positive l  )
-        _ -> return $ Nothing
-
diff --git a/Satchmo/Solver/Qube.hs b/Satchmo/Solver/Qube.hs
deleted file mode 100644
--- a/Satchmo/Solver/Qube.hs
+++ /dev/null
@@ -1,43 +0,0 @@
-module Satchmo.Solver.Qube
-
-( solve
-)
-
-where
-
-import Satchmo.Data
-import qualified Satchmo.Solve
-import Satchmo.Solver.Internal
-import Satchmo.SAT
-
-import qualified Data.ByteString.Char8 as S
-import qualified Data.ByteString.Lazy.Char8 as BS
-
-import Data.Monoid
-import System.IO (stderr, hPutStrLn)
-import System.Process
-import Control.Monad ( when )
-
-import qualified Data.Map as M
-
-solve = Satchmo.Solve.solve qube
-
-qube :: Satchmo.Solve.Implementation
-qube cs Header{numVars=numVars, numClauses=numClauses} = do
-    let header = mkDimacsHeader numVars numClauses
-    let debug = True
-    if debug 
-       then BS.hPut stderr cs
-       else hPutStrLn stderr header
-    ( code, stdout, stderr ) <- 
-        readProcessWithExitCodeBS "QuBE6.5" [ "/dev/stdin" ] (BS.pack header `mappend` cs)
-    when debug $ hPutStrLn System.IO.stderr stdout
-    let 
-    case filter ( \ ws -> take 1 ws /= [ "c" ] ) $ map words $ lines stdout of
-        [ "s", "cnf", "1" ] : rest -> 
-            return $ Just $ M.fromList $ do
-                "v" : vars <- rest
-                l <- map read $ takeWhile ( /= "0" ) vars
-                return ( variable l, positive l )
-        _ -> return $ Nothing
-
diff --git a/Satchmo/Solver/Yices.hs b/Satchmo/Solver/Yices.hs
--- a/Satchmo/Solver/Yices.hs
+++ b/Satchmo/Solver/Yices.hs
@@ -7,8 +7,7 @@
 
 where
 
-import qualified Data.ByteString.Char8 as S
-import qualified Data.ByteString.Lazy.Char8 as BS
+import qualified Data.ByteString.Char8 as BS
 import Data.Monoid
 import Satchmo.Data
 import qualified Satchmo.Solve
@@ -21,7 +20,8 @@
 import System.Process
 import Control.Monad ( when )
 
-import qualified Data.Map as M
+-- import qualified Data.Map as M
+import qualified Data.Array as A
 
 type Seconds = Int
 
@@ -31,18 +31,19 @@
 yices :: Maybe Seconds -> Satchmo.Solve.Implementation
 yices timeout cs Header{numVars=numVars, numClauses=numClauses} = do
     let header = mkDimacsHeader numVars numClauses
-    let debug = False
+    let debug = True
     if debug
        then BS.hPut stderr cs
        else hPutStrLn stderr header >> hFlush stderr
 
     let opts = ["-e","-d"] ++ maybe [] (\t -> ["-tm", show t]) timeout
 
-    ( code, stdout, stderr ) <- readProcessWithExitCodeBS "yices" opts (BS.pack header `mappend` cs)
+    ( code, stdout, stderr ) <- 
+        readProcessWithExitCodeS "yices" opts (BS.pack header `mappend` cs)
     when debug $ hPutStrLn System.IO.stderr stdout
     when (not $ null stderr) $ putStrLn stderr
     case lines stdout of
-        "sat" : xs : _ -> return $ Just $ M.fromList $ do
+        "sat" : xs : _ -> return $ Just $ A.array (1, numVars) $ do
             l :: Literal <- map read $ words xs
             return ( variable l, positive l )
         _ -> return $ Nothing
@@ -57,11 +58,11 @@
 
     let opts =  ["-e","-d","-ms", "-mw", show maxWeight] ++ maybe [] (\t -> ["-tm", show t]) timeout
 
-    ( code, stdout, stderr ) <- readProcessWithExitCodeBS "yices" opts (BS.pack header `mappend` cs)
+    ( code, stdout, stderr ) <- readProcessWithExitCodeS "yices" opts (BS.pack header `mappend` cs)
     when debug $ hPutStrLn System.IO.stderr stdout
     when (not $ null stderr) $ putStrLn stderr
     case lines stdout of
-        "sat" : xs : _ -> return $ Just $ M.fromList $ do
+        "sat" : xs : _ -> return $ Just $ A.array (1, Weighted.numVars h) $ do
             l <- map read $ words xs
             return ( variable l, positive l )
         _ -> return $ Nothing
diff --git a/satchmo-backends.cabal b/satchmo-backends.cabal
--- a/satchmo-backends.cabal
+++ b/satchmo-backends.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo-backends
-Version:        1.8.2
+Version:        1.9.1
 
 License:        GPL
 License-file:	gpl-2.0.txt
@@ -19,15 +19,14 @@
 build-type: Simple
 
 library
-    Build-depends: satchmo >= 1.8, process, base == 4.* , containers, bytestring
+    Build-depends: satchmo >= 1.8, process, base == 4.* , containers, array, bytestring, timeit
     Exposed-modules:
         Satchmo.Solver.Minisat
         Satchmo.Solver.Pcosat
-        Satchmo.Solver.Clasp
-        Satchmo.Solver.Quantor
-        Satchmo.Solver.Qube
+        -- Satchmo.Solver.Clasp
+        -- Satchmo.Solver.Quantor
+        -- Satchmo.Solver.Qube
         Satchmo.Solver.Yices
     Other-modules:
         Satchmo.Solver.Internal
     hs-source-dirs:	.
-