diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,5 +1,5 @@
 Name:          cflp
-Version:       2009.1.24
+Version:       2009.1.26
 Cabal-Version: >= 1.6
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
@@ -21,18 +21,17 @@
 Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs
 
 Library
-  Build-Depends:    base >= 4, 
-                    containers, 
-                    value-supply, 
-                    mtl, 
-                    syb, 
+  Build-Depends:    base >= 4, mtl, syb, containers,
+                    control-monad-omega, logict,
+                    random, MonadRandom,
+                    value-supply,
                     HUnit
   Exposed-Modules:  CFLP
                     CFLP.Strategies
                     CFLP.Strategies.CallTimeChoice
                     CFLP.Strategies.DepthCounter
-                    CFLP.Strategies.DepthFirst
                     CFLP.Strategies.DepthLimit
+                    CFLP.Strategies.Random
                     CFLP.Tests
                     CFLP.Tests.CallTimeChoice
                     CFLP.Tests.HigherOrder
diff --git a/src/CFLP.lhs b/src/CFLP.lhs
--- a/src/CFLP.lhs
+++ b/src/CFLP.lhs
@@ -19,7 +19,7 @@
 >
 >   eval, evalPartial, evalPrint,
 >
->   Monadic(..), UpdateT,
+>   Monadic, monadic, UpdateT,
 >
 >   module CFLP.Data
 >
@@ -45,6 +45,9 @@
 >                          , Enumerable (Res s))
 >    => CFLP s
 >
+> monadic :: Monad m => Monadic (UpdateT c m) ()
+> monadic = Monadic (return ())
+>
 > instance (MonadPlus m, Enumerable m) => CFLP (Monadic (UpdateT () m))
 
 We define a shortcut for types of constraint functional-logic data and
@@ -67,13 +70,13 @@
     solutions of a constraint functional-logic computation.
 
 > eval, evalPartial
->   :: (Monad s, CFLP s, Generic a) => s (Ctx s) -> Computation a -> IO [a]
-> eval        s = liftM (liftM primitive) . evaluate s (groundNormalForm s)
-> evalPartial s = liftM (liftM primitive) . evaluate s (partialNormalForm s)
+>   :: (Monad s, CFLP s, Generic a) => [s (Ctx s)] -> Computation a -> IO [a]
+> eval        s = liftM (liftM primitive) . evaluate s groundNormalForm
+> evalPartial s = liftM (liftM primitive) . evaluate s partialNormalForm
 >
 > evalPrint :: (Monad s, CFLP s, Generic a)
->           => s (Ctx s) -> Computation a -> IO ()
-> evalPrint s op = evaluate s (partialNormalForm s) op >>= printSols
+>           => [s (Ctx s)] -> Computation a -> IO ()
+> evalPrint s op = evaluate s partialNormalForm op >>= printSols
 >
 > printSols :: Show a => [a] -> IO ()
 > printSols []     = putStrLn "No more solutions."
@@ -91,11 +94,11 @@
 constraint functional-logic computation according to a given strategy.
 
 > evaluate :: CFLP s
->          => s (Ctx s)
->          -> (Nondet (Ctx s) s a -> Res s b)
+>          => [s (Ctx s)]
+>          -> (s (Ctx s) -> Nondet (Ctx s) s a -> Res s b)
 >          -> Computation a
 >          -> IO [b]
 > evaluate s evalNondet op = do
 >   i <- initID
->   return $ enumeration $
->     evalNondet (Typed (s >>= untyped . flip op i . Context))
+>   return $ concatMap enumeration $
+>     map (\c -> evalNondet c (Typed (c >>= untyped . flip op i . Context))) s
diff --git a/src/CFLP/Strategies.lhs b/src/CFLP/Strategies.lhs
--- a/src/CFLP/Strategies.lhs
+++ b/src/CFLP/Strategies.lhs
@@ -10,33 +10,66 @@
 >
 > module CFLP.Strategies (
 >
->   dfs, limDFS,
->
->   module CFLP.Strategies.DepthFirst,
->   module CFLP.Strategies.CallTimeChoice,
->   module CFLP.Strategies.DepthCounter,
->   module CFLP.Strategies.DepthLimit
+>   dfs, limDFS, iterDFS, diag, rndDFS
 >
 >  ) where
 >
-> import Control.Monad
+> import Control.Monad.Omega
+> import Control.Monad.Logic
 >
 > import CFLP
-> import CFLP.Strategies.DepthFirst
 > import CFLP.Strategies.CallTimeChoice
 > import CFLP.Strategies.DepthCounter
 > import CFLP.Strategies.DepthLimit
+> import CFLP.Strategies.Random
 
 We provide shortcuts for useful strategies.
 
-> dfs :: CTC (Monadic (UpdateT (StoreCTC ()) [])) (StoreCTC ())
-> dfs = callTimeChoice dfsWithEvalTimeChoice
+depth-first search:
+
+> instance Enumerable []    where enumeration = id
+> instance Enumerable Logic where enumeration = observeAll
 >
-> limDFS :: Int -> CTC (Depth (DepthLim (Monadic
->                       (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) []))))
->                       (StoreCTC (DepthCtx (DepthLimCtx ())))
-> limDFS l = callTimeChoice.countDepth.limitDepth l$dfsWithEvalTimeChoice
+> dfs :: [CTC (Monadic (UpdateT (StoreCTC ()) Logic)) (StoreCTC ())]
+> dfs = [callTimeChoice monadic]
 
+depth-first search with limited depth:
+
+> limDFS :: Int
+>        -> [CTC (Depth (DepthLim (Monadic
+>                 (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) Logic))))
+>                (StoreCTC (DepthCtx (DepthLimCtx ())))]
+> limDFS l = [limitedDepthFirstSearch l]
+>
+> limitedDepthFirstSearch
+>  :: Int -> CTC (Depth (DepthLim (Monadic
+>                  (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) Logic))))
+>                (StoreCTC (DepthCtx (DepthLimCtx ())))
+> limitedDepthFirstSearch l
+>   = callTimeChoice . countDepth . limitDepth l $ monadic
+
+iterative deepening depth-first search:
+
+> iterDFS :: [CTC (Depth (DepthLim (Monadic
+>                   (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) Logic))))
+>                 (StoreCTC (DepthCtx (DepthLimCtx ())))]
+> iterDFS = map limitedDepthFirstSearch [0..]
+
+Fair diagonalization by Luke Palmer:
+
+> instance Enumerable Omega where enumeration = runOmega
+>
+> diag :: [CTC (Monadic (UpdateT (StoreCTC ()) Omega)) (StoreCTC ())]
+> diag = [callTimeChoice monadic]
+
+We combine randomization with depth-first search. Here, it is crucial
+to use the call-time choice transformer *before* the randomizer
+shuffles choices.
+
+> rndDFS :: [CTC (Rnd (Monadic (UpdateT (StoreCTC (RndCtx ())) Logic)))
+>                (StoreCTC (RndCtx ()))]
+> rndDFS = [callTimeChoice . randomise $ monadic]
+
 Finally, we provide instances for the type class `CFLP` that is a
 shortcut for the class constraints of CFLP computations.
 
@@ -46,4 +79,7 @@
 > instance (MonadPlus m, Enumerable m)
 >       => CFLP (CTC (Depth (DepthLim (Monadic
 >                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) m)))))
+>
+> instance (MonadPlus m, Enumerable m)
+>       => CFLP (CTC (Rnd (Monadic (UpdateT (StoreCTC (RndCtx ())) m))))
 
diff --git a/src/CFLP/Strategies/DepthFirst.lhs b/src/CFLP/Strategies/DepthFirst.lhs
deleted file mode 100644
--- a/src/CFLP/Strategies/DepthFirst.lhs
+++ /dev/null
@@ -1,31 +0,0 @@
-% Depth-First Search for Constraint Functional-Logic Programs
-% Sebastian Fischer (sebf@informatik.uni-kiel.de)
-
-This module defines depth-first search as a strategy that can be used
-in constraint functional-logic programs.
-
-It shows what definitions are necessary in order to turn an instance
-of the `MonadPlus` type class into a strategy for CFLP.
-
-> {-# LANGUAGE
->       FlexibleInstances
->   #-}
->
-> module CFLP.Strategies.DepthFirst where
->
-> import CFLP
-
-Depth-first search is implemented by the list monad. In order to make
-it a strategy, we need to make `[]` an instance of the `Enumerable`
-type class that allows to enumerate monadic values in a list. For the
-list monad, this instance is trivial:
-
-> instance Enumerable [] where enumeration = id
-
-We define depth-first search strategies for evaluation-time choice
-semantics. In order to get call-time choice, this needs to be
-transformed with the call-time choice transformer.
-
-> dfsWithEvalTimeChoice :: Monadic (UpdateT c []) ()
-> dfsWithEvalTimeChoice = Monadic (return ())
-
diff --git a/src/CFLP/Strategies/Random.lhs b/src/CFLP/Strategies/Random.lhs
new file mode 100644
--- /dev/null
+++ b/src/CFLP/Strategies/Random.lhs
@@ -0,0 +1,107 @@
+% Randomization for CFL Computations
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module provides a strategy transformer that randomly reorders
+choices in the search space.
+
+> {-# LANGUAGE
+>       GeneralizedNewtypeDeriving,
+>       MultiParamTypeClasses,
+>       OverlappingInstances,
+>       FlexibleInstances,
+>       TypeFamilies
+>   #-}
+>
+> module CFLP.Strategies.Random (
+>
+>   Randomiser(..), Rnd, RndCtx, randomise
+>
+>  ) where
+>
+> import Control.Monad
+> import Control.Monad.Random
+>
+> import CFLP.Control.Monad.Update
+>
+> import CFLP.Control.Strategy
+
+The interface of an evaluation context that can reorder choices
+randomly is given by the following type class.
+
+> class Randomiser c
+>  where
+>   getRandomGen :: c -> StdGen
+>   setRandomGen :: c -> StdGen -> c -> c
+
+The first argument of `setRandomGen` will always be ignored and is
+only used to support the type checker.
+
+We define uniform liftings for randomisers over arbitrary context
+transformers.
+
+> instance (Randomiser c, Transformer t) => Randomiser (t c)
+>  where
+>   getRandomGen = getRandomGen . project
+>
+>   setRandomGen _ r c = replace c (setRandomGen undefined r (project c))
+
+A random context adds a counter for the depth.
+
+> data RndCtx c = RndCtx StdGen c
+
+It is an instance of `Randomiser`.
+
+> instance Randomiser (RndCtx c)
+>  where
+>   getRandomGen     (RndCtx r _) = r
+>   setRandomGen _ r (RndCtx _ c) = RndCtx r c
+
+It also is a transformer for evaluation contexts
+
+> instance Transformer RndCtx
+>  where
+>   project (RndCtx _ c) = c
+>   replace (RndCtx d _) = RndCtx d
+
+We define a strategy transformer for depth counting.
+
+> newtype Rnd s a = Rnd { fromRnd :: s a }
+>  deriving (Monad, MonadPlus, Enumerable)
+>
+> type instance Ctx (Rnd s) = RndCtx (Ctx s)
+> type instance Res (Rnd s) = Rnd (Res s)
+
+The strategy-transformer instance shuffles each non-deterministic
+choice.
+
+> instance Randomiser c => StrategyT c Rnd
+>  where
+>   liftStrategy _ = Rnd
+>   baseStrategy _ = fromRnd
+>
+>   extendChoices c _ xs =
+>     evalRand (shuffle xs >>= mapM (setRndGen c)) (getRandomGen c)
+>
+> shuffle :: MonadRandom rnd => [a] -> rnd [a]
+> shuffle xs = shuffleWithLen (length xs) xs
+>
+> shuffleWithLen :: MonadRandom rnd => Int -> [a] -> rnd [a]
+> shuffleWithLen 0   _  = return []
+> shuffleWithLen len xs = do
+>   let len_1 = len-1
+>   n <- getRandomR (0,len_1)
+>   let (ys,z:zs) = splitAt n xs
+>   liftM (z:) (shuffleWithLen len_1 (ys++zs))
+>
+> setRndGen :: (Randomiser c, Monad m, MonadUpdate c m)
+>           => c -> m a -> Rand StdGen (m a)
+> setRndGen c x = do
+>   r <- getSplit
+>   return (update (return . setRandomGen c r) >> x)
+
+The operation `random` adds randomisation to a strategy.
+
+> randomise :: Monad s => s c -> Rnd s (RndCtx c)
+> randomise = Rnd . liftM (RndCtx (mkStdGen 42))
+
+