diff --git a/examples/Queens2.hs b/examples/Queens2.hs
new file mode 100644
--- /dev/null
+++ b/examples/Queens2.hs
@@ -0,0 +1,69 @@
+{-
+the N Queens problem (alternative implementation).
+The propositional variables
+correspond to the positions on the board.
+It shows how to construct an OBDD
+and how to check some of its properties.
+It also shows that the implementation is not terribly efficient.
+It computes the number of solutions for board size 8
+(the answer is: 92) in approx. 1.6 seconds on my machine.
+
+BUILD:  ghc -O2 Queens
+RUN  :  ./Queens 8
+-}
+
+import Prelude hiding ((&&),(||),not,and,or)
+import OBDD 
+
+import Control.Monad ( guard )
+import System.Environment ( getArgs )
+import qualified Data.Set 
+import qualified Data.Map.Strict as M
+
+type Position = (Int,Int)
+
+positions :: Int -> [ Position ]
+positions n = do 
+    a <- [ 1 .. n ]
+    b <- [ 1 .. n ]
+    return (a,b)
+
+board :: Int -> OBDD Position
+board n = and 
+    [ handle exactlyone (\(x,y) -> x) n
+    , handle atmostone  (\(x,y) -> y) n
+    , handle atmostone  (\(x,y) -> x+y) n
+    , handle atmostone  (\(x,y) -> x-y) n
+    ]
+
+atmostone xs =
+  let go (n,o) [] = n || o
+      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs
+  in  go (true,false) xs
+
+exactlyone xs =
+  let go (n,o) [] = o
+      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs
+  in  go (true,false) xs
+
+handle check f n = OBDD.and $ do
+    (k,v) <- M.toList $ M.fromListWith (++)
+          $ map (\p -> (f p, [variable p])) $ positions n
+    return $ check v
+
+main = do
+    args <- getArgs
+    case map read args :: [Int] of
+        [] -> mainf 8
+        [arg] -> mainf arg
+
+mainf n = do
+    let d :: OBDD Position
+        d = board n
+    putStrLn $ unwords [ "board size", show n ]
+    putStrLn $ unwords [ "BDD size", show $ OBDD.size d ]
+    putStrLn $ unwords [ "number of models"
+                       , show $ OBDD.number_of_models 
+                         ( Data.Set.fromList $ positions n )
+                         d
+                       ]
diff --git a/examples/Sort.hs b/examples/Sort.hs
new file mode 100644
--- /dev/null
+++ b/examples/Sort.hs
@@ -0,0 +1,234 @@
+{-# language LambdaCase #-}
+
+import Prelude hiding ((&&),(||),not,and,or,Num)
+import qualified Prelude
+import qualified Data.Bool 
+import OBDD hiding (size)
+import qualified OBDD as O
+
+import Control.Monad ( guard, forM_, when, void, mzero, msum )
+import System.Environment ( getArgs )
+import System.IO (hFlush, stdout)
+import qualified Data.Set as S
+import qualified Data.Map.Strict as M
+import Data.List (sort, sortOn, tails, transpose)
+import qualified Data.Tree as T
+import Data.Maybe (isJust)
+
+import Debug.Trace
+
+-- | we will talk about permutation matrices,
+-- so we need to index their elements.
+type Bit = OBDD (Int,Int)
+
+ispermutation :: [[Bit]] -> Bit
+ispermutation xss =
+     ( and $ map exactlyone xss )
+  && ( and $ map exactlyone $ transpose xss )
+
+exactlyone :: [Bit] -> Bit
+exactlyone xs =
+  let go (n,o) [] = o
+      go (n,o) (x:xs) = go (bool n false x, bool o n x) xs
+  in  go (true,false) xs
+
+-- | (weakly) increasing sequence of bits
+type Num = [Bit] 
+
+-- | produce a number from a sequence that has exactly one bit set.
+number :: [Bit] -> [Bit]
+number (x:xs) = scanl (||) x xs
+
+lt :: Num -> Num -> Bit
+lt xs ys = or $ zipWith (\x y -> not x && y) xs ys
+
+leq :: Num -> Num -> Bit
+leq xs ys = and $ zipWith implies xs ys
+
+type Comp = (Int,Int)
+
+comparators :: Int -> [Comp]
+comparators w =
+  [0 .. w-2] >>= \ x -> [x+1..w-1] >>= \ y -> [(x,y)]
+
+compat :: [Num] -> Comp -> Bit
+compat ns (lo,hi) = leq (ns !! lo) (ns !! hi)
+
+input w = do
+  i <- [1..w]
+  return $ map (\j -> variable (i,j))[1..w]
+
+vars w = S.fromList $ (,) <$> [1..w] <*> [1..w]
+
+-- * poset enumeration
+
+data State =
+     State { comps:: ! [Comp]
+           , poset :: ! Poset
+           , args :: ! [Num]
+           , form :: ! Bit
+           , size :: ! Integer
+           }
+
+start w =
+  let i = input w
+      f = ispermutation i
+  in State { comps = []
+           , poset = mkposet []
+           , args = map number i
+           , form = f
+           , size = number_of_models (vars w) f
+           }
+
+next :: Int -> State -> Comp -> State
+next w s c =
+  let cs' = c : comps s
+      f = compat (args s) c && form s
+  in  s { comps = cs'
+        , poset = -- mkposet cs'
+	    transitive_closure $ S.insert c $ poset s
+        , form = f
+        , size = number_of_models (vars w) f
+        }
+
+run w d = do
+  putStrLn $ unwords [ "sort", show w, "items", "with", show d, "comparisons" ]
+  (r, cache) <- work w d (start w) M.empty
+  putStrLn ""
+  putStrLn $ unwords [ "sort", show w, "items", "with", show d, "comparisons", "is"
+     , Data.Bool.bool "IMPOSSIBLE" "POSSIBLE" r ]
+  putStrLn $ unwords [ "cache", "with", show (M.size cache), "entries" ]
+  when False $ forM_ (M.toList cache) $ \(k,v) -> do
+    putStrLn $ unwords [ show k, "=>", show v ]
+    -- forM_ (M.toList m) print
+  return r
+
+work w d s known = do
+  -- print (d,comps s,size s)
+  if size s == 1
+    then return (True,known)
+    else if size s > 2^d
+         then return (False,known)
+         else do
+	   let verbose = False
+           case M.lookup (canonical $ poset s) known of
+             Just (r,prev) -> do
+               if verbose
+	         then putStrLn $ unwords [ show d, show $ size s, show (comps s)
+                                  , show r, "iso", show prev ]
+		 else putStr "!"
+               return (r,known)
+             Nothing -> do
+               let go [] known = return (False, known)
+                   go (c@(x,y):cs) known = do
+		     let [s1,s2] = reverse
+		                 $ sortOn size
+		                 $ map (next w s) [ (x,y), (y,x) ]
+                     (a1,k1) <- work w (d-1) s1 known
+                     if a1
+                       then do
+                         (a2,k2) <- work w (d-1) s2 k1
+                         if a2
+                           then return (True, k2)
+                           else go cs k2
+                       else do
+                         go cs k1
+               let candidates =
+                     filter (\ (x,y) -> Prelude.not $ S.member (x,y) $ poset s)
+                     $ filter (\ (x,y) -> Prelude.not $ S.member (y,x) $ poset s)
+                      $ comparators w
+               (r,known) <- go candidates known
+               if verbose
+	         then putStrLn $ unwords [ show d, show $ size s, show (comps s)
+                                  , show r ]
+                 else putStr "." 
+  	       hFlush stdout	 
+               return
+                 (r, M.insert (canonical $ poset s) (r, comps s) known)
+
+-- * main
+
+main = getArgs >>= \ case
+  [ ] -> void $ run 4 5
+  [ w ] -> let b = ceiling
+                 $ logBase 2 $ fromIntegral
+                 $ factorial $ read w
+           in -- search (read w) b
+	       void $ run (read w) b
+  [ w , d ] -> void $ run (read w) (read d)
+
+
+search w d = run w d >>= \ case
+  True -> return ()
+  False -> search w (d+1)
+  
+factorial n = product [1 .. n]
+
+-- * posets and their isomorphisms
+
+type Poset = S.Set Comp
+
+mkposet comps = transitive_closure $ S.fromList comps
+
+dot :: Poset -> Poset -> Poset
+dot p q = S.fromList $ do
+  (x,y1) <- S.toList p
+  (y2,z) <- S.toList q
+  guard $ y1 == y2
+  return (x,z)
+
+transitive_closure :: Poset -> Poset
+transitive_closure p =
+  let q = S.union p $ dot p p
+  in  if p == q then p else transitive_closure q
+      
+inputs  p x = map fst $ filter ((== x) . snd) $ S.toList p
+outputs p x = map snd $ filter ((== x) . fst) $ S.toList p
+
+elements p = S.union ( S.map fst p ) (S.map snd p )
+
+-- | the Int is the length, and it is used to speed up
+-- the derived Eq and Ord instance.
+data List a = List !Int ![a] deriving (Eq, Ord, Show)
+
+nil :: List a
+nil = List 0 []
+
+cons :: a -> List a -> List a
+cons x (List n xs) = List (n+1) (x:xs)
+
+list :: [a] -> List a
+list xs = List (length xs) xs
+
+instance Functor List where
+  fmap f (List n xs) = List n (map f xs)
+
+data Type = Dot | Type (List Type) (List Type) deriving (Eq, Ord, Show)
+
+types :: Poset -> M.Map Int Type
+types p = M.fromList $ zip (S.toList $ elements p) $ repeat Dot
+
+refine :: Poset ->   M.Map Int Type -> M.Map Int Type
+refine p t = M.fromList $ do
+  x <- S.toList $ elements p
+  return (x, Type ( list $ sort $ map (t M.!) $ inputs  p x )
+                  ( list $ sort $ map (t M.!) $ outputs p x ) )
+
+classes :: M.Map Int Type -> M.Map Type (S.Set Int)
+classes m = M.fromListWith S.union $ do
+  (k,v) <- M.toList m
+  return (v, S.singleton k)
+
+-- | compare with keys
+essence t = M.toAscList $ M.map S.size $ classes t
+
+canonical po =
+  let go t p =
+        let t' = refine po t
+            c' = classes t
+            p' = sort $ M.elems c'
+        in  if p == p' then M.map S.size c' else go t' p'
+  in  go (types po) []
+
+
+               
diff --git a/obdd.cabal b/obdd.cabal
--- a/obdd.cabal
+++ b/obdd.cabal
@@ -1,5 +1,5 @@
 Name:                obdd
-Version:             0.3.3
+Version:             0.4.0
 Cabal-Version:       >= 1.8
 Build-type: Simple
 Synopsis:            Ordered Reduced Binary Decision Diagrams
@@ -17,7 +17,7 @@
     Location: git://github.com/jwaldmann/haskell-obdd.git
 
 Library
-    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array
+    Build-Depends:       base==4.*, random, mtl, containers>=0.5, array, process
     Hs-Source-Dirs:	     src
     Exposed-Modules:     OBDD OBDD.Data OBDD.Make OBDD.Operation OBDD.Property
     Other-Modules:	     OBDD.IntIntMap, OBDD.VarIntIntMap
@@ -35,4 +35,16 @@
     Main-Is: Queens.hs
     Build-Depends: base, containers, obdd
 
+test-suite obdd-queens2
+    Hs-Source-Dirs : examples
+    Type: exitcode-stdio-1.0
+    Main-Is: Queens2.hs
+    Build-Depends: base, containers, obdd
+    
+test-suite obdd-sort
+    Hs-Source-Dirs : examples
+    Type: exitcode-stdio-1.0
+    Main-Is: Sort.hs
+    Build-Depends: base, containers, obdd
+    Ghc-Options: -rtsopts    
 
diff --git a/src/OBDD.hs b/src/OBDD.hs
--- a/src/OBDD.hs
+++ b/src/OBDD.hs
@@ -1,16 +1,17 @@
--- | reduced ordered binary decision diagrams
+-- | Reduced ordered binary decision diagrams,
+-- pure Haskell implementation.
 -- (c) Johannes Waldmann, 2008
 --
--- this module is intended to be imported qualified
+-- This module is intended to be imported qualified
 -- because it overloads some Prelude names.
 --
--- for a similar, but much more elaborate project, see
+-- For a similar, but much more elaborate project, see
 -- <http://www.informatik.uni-kiel.de/~mh/lehre/diplomarbeiten/christiansen.pdf>
 -- but I'm not sure where that source code would be available.
 
 module OBDD 
 
-( OBDD 
+( OBDD, display
 , module OBDD.Property
 , module OBDD.Operation
 , module OBDD.Make
@@ -18,7 +19,7 @@
 
 where
 
-import OBDD.Data ( OBDD )
+import OBDD.Data ( OBDD, display )
 import OBDD.Property
 import OBDD.Operation
 import OBDD.Make
diff --git a/src/OBDD/Data.hs b/src/OBDD/Data.hs
--- a/src/OBDD/Data.hs
+++ b/src/OBDD/Data.hs
@@ -15,7 +15,7 @@
 , number_of_models
 , some_model, all_models
 , fold, foldM
-, toDot
+, toDot, display
 -- * for internal use
 , Node (..)
 , make
@@ -49,9 +49,10 @@
    (State, runState, evalState, get, put, gets, modify)
 import qualified System.Random
 import Control.Monad.Fix
-import Control.Monad ( forM, guard )
+import Control.Monad ( forM, guard, void )
 import qualified Control.Monad ( foldM )
-
+import System.Process
+import Data.List (isPrefixOf, isSuffixOf)
 
 import Prelude hiding ( null )
 import qualified Prelude
@@ -277,6 +278,11 @@
       register n
     _ -> register n
 
+-- | Calls the @dot@ executable (must be in @$PATH@) to draw a diagram
+-- in an X11 window. Will block until this window is closed.
+-- Window can be closed gracefully by typing  'q'  when it has focus.
+display :: Show v => OBDD v -> IO ()
+display d = void $ readProcess "dot" [ "-Tx11" ] $ toDot d
 
 -- | toDot outputs a string in format suitable for input to the "dot" program
 -- from the graphviz suite.
@@ -296,7 +302,10 @@
                           _ -> idmap IM.! i
         in id &&& getNode
 
-    mkLabel lbl = "[label=\"" ++ lbl ++ "\"];"
+    unquote s = if isPrefixOf "\"" s && isSuffixOf "\"" s
+                then init $ tail s
+                else s
+    mkLabel lbl = "[label=\"" ++ unquote lbl ++ "\"];"
 
     helper (thisId, Leaf b) = return $
         -- switch to rectangle nodes for the leaf, before going back to ovals.
diff --git a/src/OBDD/Make.hs b/src/OBDD/Make.hs
--- a/src/OBDD/Make.hs
+++ b/src/OBDD/Make.hs
@@ -2,7 +2,7 @@
 
 module OBDD.Make 
 
-( constant, unit )
+( constant, unit, variable, false, true )
 
 where
 
@@ -15,6 +15,12 @@
 constant b = make $ do
     register $ Leaf b
 
+false :: Ord v => OBDD v
+false = constant False
+
+true :: Ord v => OBDD v
+true  = constant True
+
 -- | Variable with given parity
 unit :: Ord v => v -> Bool -> OBDD v
 unit v p = make $ do
@@ -22,3 +28,5 @@
     r <- register $ Leaf $     p
     register $ Branch v l r
 
+variable :: Ord v => v -> OBDD v
+variable v = unit v True
diff --git a/src/OBDD/Operation.hs b/src/OBDD/Operation.hs
--- a/src/OBDD/Operation.hs
+++ b/src/OBDD/Operation.hs
@@ -1,8 +1,10 @@
 {-# language ScopedTypeVariables #-}
+{-# language PatternGuards #-}
 
 module OBDD.Operation 
 
 ( (&&), (||), not, and, or
+, bool, implies, equiv, xor
 , unary, binary
 , instantiate
 , exists, exists_many
@@ -23,17 +25,31 @@
 -- import Data.List ( foldl' )
 -- don't use, see below
 
-import Prelude hiding ( (&&), (||), and, or, not )
+import Prelude hiding ( (&&), (||), and, or, not, bool )
 import qualified Prelude
 
+infixr 3 &&
+
 ( && ) :: Ord v => OBDD v -> OBDD v -> OBDD v
-( && ) = binary ( Prelude.&& )
+( && ) = symmetric_binary ( Prelude.&& )
 
+infixr 2 ||
+
 ( || ) :: Ord v => OBDD v -> OBDD v -> OBDD v
-( || ) = binary ( Prelude.|| )
+( || ) = symmetric_binary ( Prelude.|| )
 
+bool :: Ord v => OBDD v -> OBDD v -> OBDD v -> OBDD v
+bool f t p = (f && not p) || (t && p)
 
+equiv :: Ord v => OBDD v -> OBDD v -> OBDD v
+equiv = symmetric_binary (==)
 
+xor :: Ord v => OBDD v -> OBDD v -> OBDD v
+xor   = symmetric_binary (/=)
+
+implies :: Ord v => OBDD v -> OBDD v -> OBDD v
+implies = binary ( <= )
+
 and :: Ord v => [ OBDD v ] -> OBDD v
 and = fold_by_size (constant True) (&&)
 -- and = foldr ( && ) ( constant True ) 
@@ -75,11 +91,27 @@
     handle x
 
 
+data Symmetricity = Asymmetric | Symmetric deriving Show
+
 binary :: Ord v
       => ( Bool -> Bool -> Bool )
       -> OBDD v -> OBDD v -> OBDD v
-binary op x y = make $ do
+binary = binary_ Asymmetric
+      
+symmetric_binary :: Ord v
+      => ( Bool -> Bool -> Bool )
+      -> OBDD v -> OBDD v -> OBDD v
+symmetric_binary = binary_ Symmetric
+
+
+binary_ :: Ord v
+      => Symmetricity
+      -> ( Bool -> Bool -> Bool )
+      -> OBDD v -> OBDD v -> OBDD v
+
+binary_ sym op x y = make $ do
     let -- register = checked_register -- for testing
+        -- handle x y | Symmetric <- sym, top x > top y = handle y x
         handle x y = cached (top x, top y) $ case ( access x , access y ) of
                     ( Leaf p , Leaf q ) -> register $ Leaf $ op p q
                     ( ax, ay ) -> case comp ax ay of