Generate the CNF of pigeonhole problem in DIMACS format. See also http://www.satcompetition.org/2009/format-benchmarks2009.html

pigeonhole.sh

#!/usr/bin/env bash

if [ "$1" = "" ]; then
  echo "Please specify the number of holes"
  echo "Usage: $0 NUMBER_OF_HOLES"
  exit
fi

num_holes="$1"
num_pigeons="$(($1 + 1))"
num_variables="$(($num_holes * $num_pigeons))"
num_variables="$(($num_pigeons + $num_holes * \
                               $num_pigeons * ($num_pigeons - 1) / 2))"

VariableOf() {
  local nth_pigeon=$1
  local nth_hole=$2
  echo "$(($num_holes * ($nth_pigeon - 1) + $nth_hole))"
}

sat="p cnf $num_variables $num_variables\n"

# Every pigeon must be in some hole.
for i in $(seq 1 $num_pigeons); do
  for j in $(seq 1 $num_holes); do
    sat="$sat $(VariableOf $i $j)"
  done
  sat="$sat 0\n"
done

# Every hole cannot have more than one pigeon.
for i in $(seq 1 $num_holes); do
  for j in $(seq 1 $(($num_pigeons - 1))); do
    for k in $(seq $(($j + 1)) $num_pigeons); do
      variable_a=$(VariableOf $j $i)
      variable_b=$(VariableOf $k $i)
      sat="$sat -$variable_a -$variable_b 0\n"
    done
  done
done

echo -e "$sat"