#!/usr/bin/env perl

$pigeons=shift;
$holes=shift;

$pigeons > 0 and $holes > 0 or die "Usage: $0 m n\n";
@formula=();

# Variables:
# x1,1 ~ 1
# ...
# xm,1 ~ m
# x1,2 ~ m+1
# ...
# xm,2 ~ 2*m
# ...
# x1,n ~ (n-1)*m+1
# ...
# xm,n ~ n*m
#
# So: xi,j ~ (j-1)*m+i

# Each pigeon has to be put into some hole.
for($i=1; $i <= $pigeons; $i++) {
  @clause=();
  for($j=1; $j <= $holes; $j++) {
    push(@clause, ($j-1)*$pigeons + $i);
  }
  push(@formula,join(" ",@clause) . " 0");
}

# At most one hole per pigeon.

for($i=1; $i <= $pigeons; $i++) {
  for($j=1; $j <= $holes; $j++) {
    for($k=1; $k <= $holes; $k++) { 
      if($k != $j) {
        push(@formula,sprintf("-%d -%d 0", ($j-1)*$pigeons + $i , ($k-1)*$pigeons + $i ));
      }
    }
  }
}

# At most one pigeon per hole.

for($i=1; $i <= $pigeons; $i++) {
  for($j=1; $j <= $holes; $j++) {
    for($k=1; $k <= $pigeons; $k++) { 
      if($k != $i) {
        push(@formula,sprintf("-%d -%d 0", ($j-1)*$pigeons + $i , ($j-1)*$pigeons + $k ));
      }
    }
  }
}

printf("p cnf %d %d\n",$pigeons*$holes,$#formula+1);
foreach (@formula)
  {
  print "$_\n";
  }
