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
@@ -1,13 +1,13 @@
 module Satchmo.Binary.Op.Common
 
 ( iszero
-, equals
+, equals, lt, le, ge, eq, gt
 , full_adder, half_adder
 )
 
 where
 
-import Prelude hiding ( and, or, not )
+import Prelude hiding ( and, or, not, compare )
 
 import qualified Satchmo.Code as C
 
@@ -24,6 +24,7 @@
 equals a b = do
     equals' ( bits a ) ( bits b )
 
+
 equals' :: Booleans -> Booleans -> SAT Boolean
 equals' [] [] = B.constant True
 equals' (x:xs) (y:ys) = do
@@ -32,6 +33,35 @@
     and [ not z, rest ]
 equals' xs [] = and $ map not xs
 equals' [] ys = and $ map not ys
+
+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 a b = compare' ( bits a ) ( bits b )
+
+compare' :: Booleans 
+         -> Booleans 
+         -> SAT ( Boolean, Boolean ) -- ^ (less, equals)
+compare' [] [] = do 
+    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 ]
+    return ( l', e' )
+compare' xs [] = do
+    x <- or xs
+    return ( not x, not x )
+compare' [] ys = do
+    y <- or ys
+    return ( y, not y )
 
 full_adder :: Boolean -> Boolean -> Boolean
            -> SAT ( Boolean, Boolean )
diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs
--- a/Satchmo/Boolean/Data.hs
+++ b/Satchmo/Boolean/Data.hs
@@ -3,7 +3,8 @@
 module Satchmo.Boolean.Data 
 
 ( Boolean, Booleans
-, boolean, constant
+, boolean, exists, forall
+, constant
 , not, assert, monadic
 )
 
@@ -42,11 +43,22 @@
         Constant {} -> return $ value b
 
 boolean :: SAT Boolean
-boolean = do
+boolean = exists
+
+exists :: SAT Boolean
+exists = do
     x <- fresh
     return $ Boolean 
            { encode = x
            , decode = asks $ \ fm -> fromJust $ M.lookup x fm
+           }
+
+forall :: SAT Boolean
+forall = do
+    x <- fresh_forall
+    return $ Boolean 
+           { encode = x
+           , decode = error "Boolean.forall cannot be decoded"
            }
 
 constant :: Bool -> SAT Boolean
diff --git a/Satchmo/Code.hs b/Satchmo/Code.hs
--- a/Satchmo/Code.hs
+++ b/Satchmo/Code.hs
@@ -22,6 +22,8 @@
 
 type Decoder a = Reader ( Map Literal Bool ) a
 
+instance Decode () () where
+    decode () = return ()
 
 instance ( Decode c a, Decode d b ) => Decode ( c,d) (a,b) where
     decode (c,d) = do a <- decode c; b <- decode d; return ( a,b)
diff --git a/Satchmo/Internal.hs b/Satchmo/Internal.hs
--- a/Satchmo/Internal.hs
+++ b/Satchmo/Internal.hs
@@ -1,7 +1,8 @@
 module Satchmo.Internal 
 
 ( SAT
-, fresh, emit
+, fresh, fresh_forall
+, emit
 , sat
 )
 
@@ -12,14 +13,18 @@
 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
       }
 
@@ -29,15 +34,38 @@
 sat m = 
     let ~( ~(a,w), accu) = runState ( runWriterT m ) start
     in  ( unlines $ unwords [ "p", "cnf", show ( next accu - 1), show ( size accu ) ]
-                    : map show w
+                  : 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
-    put $ a { next = next a + 1 }
-    return $ literal $ next a
+    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
diff --git a/Satchmo/Solve.hs b/Satchmo/Solve.hs
--- a/Satchmo/Solve.hs
+++ b/Satchmo/Solve.hs
@@ -1,3 +1,6 @@
+-- | This is the API for plugging in solver implementations.
+-- Actual implementations are in the (separate) package @satchmo-backends@
+
 module Satchmo.Solve
 
 ( solve
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        1.3
+Version:        1.4
 
 License:        GPL
 License-file:	gpl-2.0.txt
@@ -7,9 +7,10 @@
 Maintainer:	Johannes Waldmann
 Homepage:       http://dfa.imn.htwk-leipzig.de/satchmo/
 Synopsis:       SAT encoding monad
-description:	Encoding for boolean and integral constraints into CNF-SAT.
+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-minisat, satchmo-funsat)
+		requires a backend (e.g. satchmo-backends, satchmo-funsat)
+Category:	Algorithms
 Build-depends:  mtl, process, containers, base, array
 Exposed-modules:
 	Satchmo.Data