diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs
--- a/Satchmo/Boolean/Op.hs
+++ b/Satchmo/Boolean/Op.hs
@@ -1,7 +1,7 @@
 module Satchmo.Boolean.Op
 
 ( constant
-, and, or, xor, equals2, equals, implies, (||), (&&)
+, and, or, xor, xor2, equals2, equals, implies, (||), (&&)
 , fun2, fun3
 , ifThenElse, ifThenElseM
 , assert_fun2, assert_fun3
diff --git a/Satchmo/Counting/Direct.hs b/Satchmo/Counting/Direct.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Counting/Direct.hs
@@ -0,0 +1,35 @@
+-- | functions in this module have no extra variables but exponential cost.
+
+module Satchmo.Counting.Direct 
+
+( atleast
+, atmost
+, exactly
+)
+
+where
+
+import Satchmo.Boolean ( Boolean, MonadSAT )  
+import qualified Satchmo.Boolean as B
+
+import Control.Monad ( forM )
+
+select :: Int -> [a] -> [[a]]
+select 0 xs = [[]]
+select k [] = []
+select k (x:xs) =
+  select k xs ++ (map (x:) $ select (k-1) xs)
+
+atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+atleast k xs = B.or =<< forM (select k xs) B.and
+
+atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+atmost k xs = atleast (length xs - k) $ map B.not xs
+
+exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
+exactly k xs = do
+  this <- atleast k xs
+  that <- atmost k xs
+  this B.&& that
+  
+        
diff --git a/examples/Ramsey.hs b/examples/Ramsey.hs
new file mode 100644
--- /dev/null
+++ b/examples/Ramsey.hs
@@ -0,0 +1,105 @@
+-- | find colouring without complete subgraphs
+-- example usage: ./dist/build/Ramsey/Ramsey 3 3 3 16
+-- last number is size of graph,
+-- earlier numbers are sizes of forbidden cliques
+
+{-# language PatternSignatures #-}
+
+import Prelude hiding ( not, and, or, product )
+import qualified Prelude
+
+import Satchmo.Relation
+import Satchmo.Code
+import Satchmo.Boolean hiding ( implies )
+import Satchmo.Counting
+
+import qualified Satchmo.Binary as B
+
+import Satchmo.SAT.Mini
+
+import Data.List (sort, tails)
+import qualified Data.Array as A
+import Control.Monad ( guard, when, forM, foldM, void )
+import System.Environment
+import Data.Ix ( range)
+
+
+main :: IO ()
+main = do
+    argv <- getArgs
+    let ns = map read $ case argv of
+          [] -> [ "3", "3", "3", "16" ]
+          _ -> argv
+        cs = init ns 
+        n = last ns
+    Just ( p : fs ) <- solve $ ramsey cs n
+    forM ( zip [ 1.. ] fs ) $ \ (k, f) -> do 
+        putStrLn $ unwords [ "colour", show k ]
+        printA f
+    putStrLn "with isomorphism" ; printA p
+
+printA :: A.Array (Int,Int) Bool -> IO ()
+printA a = putStrLn $ unlines $ do
+         let ((u,l),(o,r)) = A.bounds a
+         x <- [u .. o]
+         return $ unwords $ do 
+             y <- [ l ..r ]
+             return $ case a A.! (x,y) of
+                  True -> "* " ; False -> ". "
+
+ramsey (cs :: [Int]) (n :: Int) = do
+    fs <- forM cs $ \ c -> 
+         relation ((1 :: Int,1 :: Int),(n,n))
+    
+    p <- relation ((1,1),(n,n))
+    -- forM fs $ isomorphism p
+
+    -- forM fs $ cyclic 3
+
+    when False $ void $ do
+        forM [ 1 .. n ] $ \ x -> 
+            forM [ x + 1 .. n ] $ \ y -> 
+                assertM $ exactly 1 $ 
+                    for fs $ \ f -> f ! (x,y) 
+    when True $ void $ do
+        forM [ 1 .. n ] $ \ x -> 
+            forM [ x + 1 .. n ] $ \ y -> 
+                assert $ for fs $ \ f -> f ! (x,y)
+
+    forM ( zip cs fs ) $ \ (c,f) -> 
+        forM ( cliquesA c [1..n] ) $ \ xs ->
+            assert $ for ( cliquesA 2 xs ) $ \ [x,y] -> not $ f ! (x,y)
+    return $ forM (p : fs) decode
+    
+isomorphism p e = do
+    assertM $ regular 1 p
+    assertM $ regular 1 $ mirror p
+    e' <- foldM product ( mirror p ) [ e, p ]
+    assertM $ implies e e'
+    assertM $ implies e' e
+
+cyclic off f = forM ( indices f ) $ \ (i,j) -> 
+    when ( off < i Prelude.&& i < j ) 
+         $ assert_fun2 (==) ( f!(i,j) ) (f!(i-off,j-off))
+
+cliquesA k xs = 
+      let -- spec:  c!(i,j) == cliques i (drop j xs)
+          bnd = ((0,0),(k, length xs))
+          c = A.array bnd $ do
+            (i,j) <- A.range bnd
+            return ( (i,j)
+                   , if i == 0 then [ [] ]
+                     else if i > length xs - j then []               
+                     else c A.! (i,j+1) 
+                          ++ map (xs !! j : ) ( c A.! (i-1,j+1))
+                   )             
+      in  c A.! (k,0)         
+
+cliques 0 xs = return []
+cliques k xs | k > length xs = []
+cliques k (x:xs) =
+    cliques k xs ++ map (x :) ( cliques (k-1) xs )
+
+for = flip map
+
+assertM this = do x <- this ; assert [x]
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,5 +1,5 @@
 Name:           satchmo
-Version:        2.9.3
+Version:        2.9.4
 
 License:        GPL
 License-file:	gpl-2.0.txt
@@ -12,7 +12,7 @@
 		(hence the "mo" in "satchmo").
 
 Category:	Logic
-cabal-version:  >= 1.6
+cabal-version:  >= 1.8
 build-type: Simple
 source-repository head
     type: git
@@ -30,6 +30,7 @@
         Satchmo.Counting
         Satchmo.Counting.Unary
         Satchmo.Counting.Binary
+        Satchmo.Counting.Direct
         Satchmo.Code
         Satchmo.Integer
         Satchmo.Binary
@@ -96,3 +97,10 @@
     hs-source-dirs:     .
     extensions: 
 
+Test-Suite Ramsey
+  Type: exitcode-stdio-1.0
+  hs-source-dirs: examples
+  Main-Is: Ramsey.hs
+  Build-Depends: base, array, satchmo
+
+