From ec9edca5fa897028095e608d04081a8b87866c36 Mon Sep 17 00:00:00 2001 From: DualFroz Date: Thu, 27 Aug 2026 09:00:00 +0200 Subject: [PATCH] feat(encode): add pigeonhole principle generator --- src/Sift/Pigeonhole.hs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 src/Sift/Pigeonhole.hs 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] ]