diff --git a/Satchmo/Relation.hs b/Satchmo/Relation.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Relation.hs
@@ -0,0 +1,14 @@
+{-# language FlexibleInstances, MultiParamTypeClasses #-}
+
+module Satchmo.Relation 
+
+( module Satchmo.Relation.Data
+, module Satchmo.Relation.Op
+, module Satchmo.Relation.Prop
+)
+
+where
+
+import Satchmo.Relation.Data
+import Satchmo.Relation.Op
+import Satchmo.Relation.Prop
diff --git a/Satchmo/Relation/Data.hs b/Satchmo/Relation/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Relation/Data.hs
@@ -0,0 +1,58 @@
+{-# language FlexibleInstances, MultiParamTypeClasses #-}
+
+module Satchmo.Relation.Data
+
+( Relation, relation, build
+, bounds, (!), indices
+, table
+) 
+
+where
+
+import Satchmo.Code
+import Satchmo.Boolean
+
+import qualified Data.Array as A
+import Data.Array hiding ( bounds, (!), indices )
+
+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 bnd = do
+    pairs <- sequence $ do 
+        p <- range bnd
+        return $ do
+            x <- boolean
+            return ( p, x )
+    return $ build bnd pairs
+
+build :: ( Ix a, Ix b ) 
+      => ((a,b),(a,b)) 
+      -> [ ((a,b), Boolean ) ]
+      -> Relation a b 
+build bnd pairs = Relation $ array bnd pairs
+
+bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))
+bounds ( Relation r ) = A.bounds r
+
+indices ( Relation r ) = A.indices r
+
+Relation r ! p = r A.! p
+
+instance (Ix a, Ix b) => Decode ( Relation a b ) ( Array (a,b) Bool ) where
+    decode ( Relation r ) = do
+        decode r
+
+table :: (Enum a, Ix a, Enum b, Ix b) 
+      => Array (a,b) Bool -> String
+table r = unlines $ do
+    let ((a,b),(c,d)) = A.bounds r
+    x <- [ a .. c ]
+    return $ unwords $ do
+        y <- [ b .. d ]
+        return $ if r A.! (x,y) then "*" else "."
+
+
diff --git a/Satchmo/Relation/Op.hs b/Satchmo/Relation/Op.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Relation/Op.hs
@@ -0,0 +1,57 @@
+{-# language FlexibleInstances, MultiParamTypeClasses #-}
+
+module Satchmo.Relation.Op
+
+( mirror
+, union
+, complement
+, product
+) 
+
+where
+
+import Prelude hiding ( and, or, not, product )
+import qualified Prelude
+
+import Satchmo.Code
+import Satchmo.Boolean
+import Satchmo.Counting
+import Satchmo.Relation.Data
+
+import Control.Monad ( guard )
+import Data.Ix
+
+mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a
+mirror r = 
+    let ((a,b),(c,d)) = bounds r
+    in  build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y))
+
+complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b
+complement r = 
+    build (bounds r) $ do i <- indices r ; return ( i, not $ r!i )
+
+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
+        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 a b = do
+    let ((ao,al),(au,ar)) = bounds a
+        ((bo,bl),(bu,br)) = bounds b
+        bnd = ((ao,bl),(au,br))
+    pairs <- sequence $ do
+        i @ (x,z) <- range bnd
+        return $ do
+            o <- monadic or $ do
+                y <- [ al .. ar ]
+                return $ and [ a!(x,y), b!(y,z) ]
+            return ( i, o )
+    return $ build bnd pairs
+
+
diff --git a/Satchmo/Relation/Prop.hs b/Satchmo/Relation/Prop.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Relation/Prop.hs
@@ -0,0 +1,51 @@
+module Satchmo.Relation.Prop
+
+( implies
+, symmetric 
+, transitive
+, irreflexive
+, regular
+)
+
+where
+
+import Prelude hiding ( and, or, not, product )
+import qualified Prelude
+
+import Satchmo.Code
+import Satchmo.Boolean
+import Satchmo.Counting
+import Satchmo.Relation.Data
+import Satchmo.Relation.Op
+
+import Control.Monad ( guard )
+import Data.Ix
+
+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 :: (Enum a, Ix a) => Relation a a -> SAT Boolean
+symmetric r = implies r ( mirror r )
+
+irreflexive :: (Enum a, Ix a) => Relation a a -> SAT Boolean
+irreflexive r = and $ do
+    let ((a,b),(c,d)) = bounds r
+    x <- [a .. c]
+    return $ Satchmo.Boolean.not $ r ! (x,x) 
+
+regular :: (Enum a, Ix a) => Int -> Relation a a -> SAT Boolean
+regular deg r = monadic and $ do
+    let ((a,b),(c,d)) = bounds r
+    x <- [ a .. c ]
+    return $ exactly deg $ do 
+        y <- [ b .. d ]
+        return $ r !(x,y)
+
+transitive :: ( Enum a, Ix a ) 
+           => Relation a a -> SAT Boolean
+transitive r = do
+    r2 <- product r r
+    implies r2 r
diff --git a/Satchmo/Solve.hs b/Satchmo/Solve.hs
--- a/Satchmo/Solve.hs
+++ b/Satchmo/Solve.hs
@@ -1,6 +1,7 @@
 module Satchmo.Solve
 
 ( solve
+, Implementation
 , Decoder
 )
 
@@ -15,14 +16,15 @@
 
 import Control.Monad.State
 import Control.Monad.Reader
-import System.Process
 
+type Implementation = String -> IO ( Maybe ( Map Literal Bool ) )
 
-solve :: SAT ( Decoder a )
+solve :: Implementation
+      -> SAT ( Decoder a )
     -> IO ( Maybe a )
-solve build = do
+solve implementation build = do
     let (s, a) = sat build
-    mfm <- run s
+    mfm <- implementation s
     case mfm of
         Nothing -> do
             putStrLn "not satisfiable"
@@ -32,18 +34,3 @@
             -- print fm
             return $ Just $ runReader a fm
                 
-run :: String -> IO ( Maybe ( Map Literal Bool ) )
-run cs = do
-    let debug = False
-    if debug 
-       then putStrLn cs
-       else putStrLn $ head $ lines cs
-    ( code, stdout, stderr ) <- 
-        readProcessWithExitCode "minisat" [ "/dev/stdin", "/dev/stdout" ] cs
-    when debug $ putStrLn stdout
-    case lines stdout of
-        "SAT" : xs : _ -> return $ Just $ M.fromList $ do
-            x <- takeWhile ( /= 0 ) $ map read $ words xs
-            let l = literal $ abs x
-            return ( l, x > 0 )
-        _ -> return $ Nothing
diff --git a/TODO b/TODO
deleted file mode 100644
--- a/TODO
+++ /dev/null
@@ -1,11 +0,0 @@
-* minisat needs to be in the $PATH (for execution),
-  this should be checked during installation.
-
-* should provide several backends (separate package satchmo-minisat etc.,
-  similar as hsql with backends like hsql-mysql etc.)
-
-* add timeout handler for calling the SAT solver.
-  
-
-* implement fixed-width integer arithmetics
-
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,6 @@
 Name:           satchmo
-Version:        1.2
+Version:        1.3
+
 License:        GPL
 License-file:	gpl-2.0.txt
 Author:         Johannes Waldmann
@@ -8,9 +9,10 @@
 Synopsis:       SAT encoding monad
 description:	Encoding for boolean and integral constraints into CNF-SAT.
 		The encoder is provided as a State monad (hence the "mo" in "satchmo").
-		Requires SAT solver "minisat" installed.
+		requires a backend (e.g. satchmo-minisat, satchmo-funsat)
 Build-depends:  mtl, process, containers, base, array
 Exposed-modules:
+	Satchmo.Data
         Satchmo.Solve
         Satchmo.Boolean
 	Satchmo.Counting
@@ -19,16 +21,15 @@
 	Satchmo.Binary.Op.Common
 	Satchmo.Binary.Op.Fixed
 	Satchmo.Binary.Op.Flexible
+	Satchmo.Relation
+	Satchmo.Relation.Data
+	Satchmo.Relation.Op
+	Satchmo.Relation.Prop
 Other-modules:
 	Satchmo.Binary.Data
         Satchmo.Boolean.Op
         Satchmo.Boolean.Data
 	Satchmo.Internal
-	Satchmo.Data
 hs-source-dirs:	.
-extra-source-files: test/Binary.hs  test/HC.hs      test/Schur.hs
-		    test/Factor.hs
-		    test/Cage.hs    test/Ramsey.hs  test/VC.hs
-		    TODO
 extensions: 
 build-type: Simple
diff --git a/test/Binary.hs b/test/Binary.hs
deleted file mode 100644
--- a/test/Binary.hs
+++ /dev/null
@@ -1,79 +0,0 @@
--- | run tests (in ghci) like this: "solve test2"
-
-import Prelude hiding ( not )
-
-import Satchmo.Boolean hiding ( constant )
-import Satchmo.Code
-
-import Satchmo.Binary.Op.Fixed
--- import Satchmo.Binary.Op.Flexible
-
-import Satchmo.Solve
-
-
-assert_positive x = do 
-    n <- constant 0 
-    e <- equals n x 
-    assert [ not e ]
-
-assert_equals x y = do 
-    e <- equals x y 
-    assert [ e ]
-
-assert_lt x y = do 
-    d <- number $ width y
-    assert_positive d
-    xd <- add x d
-    assert_equals xd y
-
-test1 = do 
-    x <- number 4 
-    y <- constant 12 
-    assert_equals x y
-    return $ decode (x,y)
-
-test2 = do 
-    x <- constant 3
-    y <- constant 9
-    z <- add x y
-    return $ decode [x,y,z]
-
-test3 = do 
-    x <- number 5 
-    xx <- add x x
-    xxx <- add xx x
-    y <- constant 15 
-    assert_equals xxx y 
-    return $ decode [ x, y ]
-
-test4 = do 
-    x <- number  8
-    y <- number  8
-    xy <- times x y
-    z <- constant 63
-    assert_equals xy z
-    return $ decode [x, y, z]
-
-test5 = do 
-    x <- number  10
-    y <- number  10
-    xy <- times x y
-    z <- constant 1001
-    assert_equals xy z
-    return $ decode [x, y, z]
-
-ramanujan = do
-    let bits = 11
-    a <- number  bits
-    b <- number  bits
-    c <- number  bits
-    d <- number  bits
-
-    assert_lt a c ; assert_lt c d ; assert_lt d b
-
-    let cube x = do x2 <- times x x ; times x2 x
-    a3 <- cube a; b3 <- cube b; ab <- add a3 b3
-    c3 <- cube c; d3 <- cube d; cd <- add c3 d3
-    assert_equals ab cd
-
-    return $ decode [a,b,c,d]
diff --git a/test/Cage.hs b/test/Cage.hs
deleted file mode 100644
--- a/test/Cage.hs
+++ /dev/null
@@ -1,58 +0,0 @@
-import Prelude hiding ( not )
-
-import Satchmo.Relation
-import Satchmo.Code
-import Satchmo.Boolean
-import Satchmo.Counting
-import Satchmo.Solve
-
-import Data.List ( inits, tails )
-import System.Environment
-
--- | command line arguments: r g n
--- program looks for a (r,g) cage:
--- r-regular graph with girth g on n nodes
-
-main :: IO ()
-main = do
-    argv <- getArgs
-    let [ r, g, n ] = map read argv
-    Just a <- solve $ cage r g n
-    putStrLn $ table a
-
-type Graph = Relation Int Int
-
-cage r g n = do
-    a <- relation ((1,1),(n,n))
-    monadic assert [ symmetric a ]
-    monadic assert [ irreflexive a ]
-    monadic assert [ regular r a ]
-    girth_at_least g a
-    return $ decode a
-
-girth_at_least :: Int -> Graph -> SAT ()
-girth_at_least k g = sequence_ $ do
-    let ((lo,_),(hi,_)) = bounds g
-    c <- [ 3 .. k-1 ]
-    xs <- sublists c [lo .. hi]
-    return $ assert_no_circle xs g
-    
-assert_no_circle xs g = 
-    assert $ do 
-        (x,y) <- zip xs $ rotate 1 xs
-        return $ not $ g ! (x,y)
-            
-sublists :: Int -> [a] -> [[a]]
-sublists 0 xs = return []
-sublists k xs = do
-    ( pre, this : post ) <- splits xs
-    that <- sublists (k-1) $ pre ++ post
-    return $ this : that
-
-splits :: [a] -> [ ([a],[a]) ]
-splits xs = zip ( inits xs ) ( tails xs )
-
-rotate :: Int -> [a] -> [a]
-rotate k xs = 
-    let ( pre, post ) = splitAt k xs
-    in  post ++ pre
diff --git a/test/Factor.hs b/test/Factor.hs
deleted file mode 100644
--- a/test/Factor.hs
+++ /dev/null
@@ -1,32 +0,0 @@
--- | attempt factorization of integer.
--- | run like this: ./test/Factor 1000000000001
--- (takes 10 .. 20 seconds depending on your CPU)
-
-import Prelude hiding ( not )
-
-import Satchmo.Binary.Op.Fixed 
-import qualified Satchmo.Binary.Op.Flexible 
-import Satchmo.Solve
-import Satchmo.Boolean 
-import Satchmo.Code
-
-import System.Environment
-
-main :: IO ()
-main = do
-    [ n ] <- getArgs
-    res <- solve $ do
-        x <- Satchmo.Binary.Op.Flexible.constant $ read n
-        a <- number $ width x 
-        notone a
-        b <- number $ width x  
-        notone b
-        ab <- times a b
-        monadic assert [ equals ab x ]
-        return $ decode [ a, b ]
-    print res
-
-notone f = do
-    one <- Satchmo.Binary.Op.Flexible.constant 1
-    e <- equals f one
-    assert [ not e ]
diff --git a/test/HC.hs b/test/HC.hs
deleted file mode 100644
--- a/test/HC.hs
+++ /dev/null
@@ -1,76 +0,0 @@
-{-# language ScopedTypeVariables #-}
-
-import Prelude hiding ( not )
-import qualified Prelude
-
-import Satchmo.Relation
-import Satchmo.Code
-import Satchmo.Boolean
-import Satchmo.Counting
-import Satchmo.Solve
-
-import Data.List (sort)
-import qualified Data.Array as A
-import Control.Monad ( guard, when )
-import System.Environment
-
--- | command line arguments: m n
--- compute knight's tour on  m x n  chess board
-
-main :: IO ()
-main = do
-    argv <- getArgs
-    let [ m, n ] = map read argv
-    Just a <- solve $ tour m n
-    putStrLn $ unlines $ do
-         let ((u,l),(o,r)) = A.bounds a
-         x <- [u .. o]
-         return $ unwords $ do 
-             y <- [ l ..r ]
-             return $ fill 4 $ show $ a A.! (x,y)
-
-fill k cs = replicate (k - length cs) ' ' ++ cs
-
-tour m n = do
-    let s = m * n
-    p :: Relation Int (Int,Int) <- bijection ((1,(1,1)), (s,(m,n)))
-    sequence_ $ do
-        (i,j) <- zip [1..s] $ rotate 1 [1..s]
-        a <- A.range ((1,1),(m,n))
-        return $ do
-            assert $ not ( p!(i,a)) : do
-                b <- A.range ((1,1),(m,n))
-                guard $ reaches a b
-                return $ p ! (j,b) 
-            assert $ not ( p!(j,a)) : do
-                b <- A.range ((1,1),(m,n))
-                guard $ reaches a b
-                return $ p ! (i,b) 
-    return $ do
-        a <- decode p
-        return $ A.array ((1,1),(m,n)) $ do
-            ((i,p),True) <- A.assocs a
-            return (p,i)
-
-bijection :: (A.Ix a, A.Ix b) 
-                   => ((a,b),(a,b)) 
-                   -> SAT ( Relation a b )
-bijection bnd = do
-    let ((u,l),(o,r)) = bnd
-    a <- relation bnd
-    sequence_ $ do
-        x <- A.range (u,o)
-        return $ monadic assert $ return $ exactly 1 $ do y <- A.range (l,r) ; return $ a!(x,y)
-    sequence_ $ do
-        y <- A.range (l,r)
-        return $ monadic assert $ return $ exactly 1 $ do x <- A.range (u,o) ; return $ a!(x,y)
-    return a                                                   
-
-reaches (px,py) (qx,qy) = 
-    5 == (px - qx)^2 + (py - qy)^2
-
-rotate :: Int -> [a] -> [a]
-rotate k xs = 
-    let ( pre, post ) = splitAt k xs
-    in  post ++ pre
-    
diff --git a/test/Ramsey.hs b/test/Ramsey.hs
deleted file mode 100644
--- a/test/Ramsey.hs
+++ /dev/null
@@ -1,83 +0,0 @@
-import Prelude hiding ( not )
-import qualified Prelude
-
-import Satchmo.Relation
-import Satchmo.Code
-import Satchmo.Boolean
-import Satchmo.Counting
-import Satchmo.Solve
-
-import Data.List ( inits, tails )
-import Data.Ix
-import qualified Data.Array as A
-import Control.Monad ( forM, guard )
-import System.Environment
-
--- | command line arguments: c_1 .. c_k n
--- program prints graph g that proves
--- R(c_1, .., c_k) > n
-
-main :: IO ()
-main = do
-    argv <- fmap ( map read ) getArgs
-    let cs = init argv
-        n  = last argv
-    Just a <- solve $ ramsey cs n
-    print a
-
-type Graph = Relation Int Int
-
-ramsey cs n = do
-    cols <- sequence $ replicate (length cs) $ do
-        r <- relation ((1,1),(n,n))
-        monadic assert [ symmetric r ]
-        monadic assert [ irreflexive r ]
-        return r
-    circular_colouring ( n `div` length cs ) cols
-    each_edge_is_coloured n cols
-    forM ( zip cs cols ) no_monochromatic_clique
-    return $ do
-        ds <- mapM decode cols
-        return $ do
-            i <- range ((1,1),(n,n))
-            let c = length $ takeWhile Prelude.not $ do d <- ds ; return $ d A.! i
-            return ( i, c )
-
-circular_colouring period cols = sequence_ $ do
-    (col, col') <- zip cols $ rotate 1 cols
-    x @ (p,q) <- indices col
-    let y = (p+period,q+period)
-    guard $ inRange ( bounds col ) y
-    return $ do
-        assert [ not $ col ! x, col' ! y ]
-
-rotate :: Int -> [a] -> [a]
-rotate k xs = 
-    let ( pre, post ) = splitAt k xs
-    in  post ++ pre
-
-each_edge_is_coloured n cols = sequence_ $ do
-    (p,q) <- range ((1,1),(n,n))
-    guard $ p < q
-    return $ assert $ do 
-            col <- cols
-            return $ col ! (p,q)
-
-no_monochromatic_clique (c, col) = sequence_ $ do
-    let ((lo,_),(hi,_)) = bounds col
-    xs <- ordered_sublists c [lo .. hi]
-    return $ assert $ do
-        x : ys <- tails xs
-        y <- ys
-        return $ not $ col!(x,y)
-
-ordered_sublists :: Int -> [a] -> [[a]]
-ordered_sublists 0 xs = return []
-ordered_sublists k xs = do
-    ( pre, this : post ) <- splits xs
-    that <- ordered_sublists (k-1) $ post
-    return $ this : that
-
-splits :: [a] -> [ ([a],[a]) ]
-splits xs = zip ( inits xs ) ( tails xs )
-
diff --git a/test/Schur.hs b/test/Schur.hs
deleted file mode 100644
--- a/test/Schur.hs
+++ /dev/null
@@ -1,65 +0,0 @@
-import Prelude hiding ( not, or, and )
-
-import Satchmo.Relation
-import Satchmo.Code
-import Satchmo.Boolean
-import Satchmo.Counting
-import Satchmo.Solve
-
-import Data.List ( inits, tails )
-import qualified Data.Array as A
-import System.Environment
-import Control.Monad ( guard, forM_ )
-
--- | command line arguments: c n
--- program looks for sum-free c-colouring of [1 .. n]
-
-main :: IO ()
-main = do
-    argv <- getArgs
-    let [ c, n ] = map read argv
-    Just a <- solve $ schur c n
-    putStrLn $ table a
-    print $ do
-        o <- [ 1 .. c ]
-        return ( o, length $ do i <- [ 1 .. n ]; guard $ a A.! (i,o) )
-
-schur c n = do
-    col <- relation ((1,1),(n,c))
-    each_number_coloured col
-    sum_free_colouring col
-    return $ decode col
-
-periodic p col = sequence_ $ do
-    let ((1,1),(n,c)) = bounds col
-    x <- [ 1 .. n ]
-    let y = x + p
-    guard $ y <= n
-    o <- [ 1 .. c ]
-    let p = 1 + o `mod` c
-    return $ assert [ not $ col!(x,o), col!(y,p) ]
-
-each_number_coloured col = sequence_ $ do
-    let ((1,1),(n,c)) = bounds col
-    x <- [ 1 .. n ]
-    return $ assert $ do o <- [1 .. c]; return $ col!(x,o)
-
-sum_free_colouring col = sequence_ $ do
-    let ((1,1),(n,c)) = bounds col
-    x <- [ 1 .. n ]
-    y <- [ x .. n ]
-    let z = (x + y) `mod` (n+1)
-    guard $ z <= n
-    guard $ 1 <= z
-    o <- [1 .. c]
-    return $ assert $ do 
-        p <- [ x, y, z ]
-        return $ not $ col!(p,o)
-
-evenly_distributed col = do
-    let ((1,1),(n,c)) = bounds col
-        d = n `div` c
-    forM_ [ 1 .. c ] $ \ o -> do
-        a <- atleast d $ do i <- [ 1 .. n ] ; return $ col!(i,o)
-        assert [a]
-
diff --git a/test/VC.hs b/test/VC.hs
deleted file mode 100644
--- a/test/VC.hs
+++ /dev/null
@@ -1,42 +0,0 @@
-import Prelude hiding ( not )
-
-import Satchmo.Relation
-import Satchmo.Code
-import Satchmo.Boolean
-import Satchmo.Counting
-import Satchmo.Solve
-
-import Control.Monad ( guard )
-import System.Environment
-import System.Timeout
-
--- | command line arguments: n s
--- compute vertex cover of size <= s for knight's graph on  n x n  chess board
-
-main :: IO ()
-main = do
-    argv <- getArgs
-    let [ n, s ] = map read argv
-    -- this is just to check whether time-outing works
-    -- Just (Just a) <- timeout (10^6) $ solve $ knight n s
-
-    Just a <- solve $ knight n s
-    putStrLn $ table a
-
-knight n s = do
-    a <- relation ((1,1),(n,n))
-    m <- atmost s $ do 
-           i <- indices a ; return $ a ! i
-    assert [m]
-    sequence_ $ do
-        p <- indices a
-        return $ assert $ do
-            q <- indices a
-            guard $ p == q || reaches p q
-            return $ a!q
-    return $ decode a
-        
-reaches (px,py) (qx,qy) = 
-    5 == (px - qx)^2 + (py - qy)^2
-
-