diff --git a/src/Sift/Pigeonhole.hs b/src/Sift/Pigeonhole.hs
new file mode 100644
index 0000000..ebeb6e6
--- /dev/null
+++ b/src/Sift/Pigeonhole.hs
@@ -0,0 +1,20 @@
+module Sift.Pigeonhole
+  ( pigeonhole
+  ) where
+
+import Sift.Types
+
+-- pigeonhole pigeons holes encodes: every pigeon sits in some hole, and no two
+-- pigeons share a hole. With pigeons > holes the formula is UNSAT.
+pigeonhole :: Int -> Int -> CNF
+pigeonhole pigeons holes = CNF (atLeastOne ++ atMostOne)
+  where
+    cell p h = Var ((p - 1) * holes + h)
+    atLeastOne =
+      [ [ posLit (cell p h) | h <- [1 .. holes] ]
+      | p <- [1 .. pigeons] ]
+    atMostOne =
+      [ [ negLit (cell p h), negLit (cell q h) ]
+      | h <- [1 .. holes]
+      , p <- [1 .. pigeons]
+      , q <- [p + 1 .. pigeons] ]