use 5.010;

# produces PHP(m,n)
my $n=11;   # pigeons
my $m=10;   # holes

open(OUT,">pigeonhole.sat");
say OUT "c PHP($n,$m)";
my $x=$n*$m;
my $y=$n*$n*$m;
say OUT "p cnf $x $y";
for(my $i=1;$i<=$n;$i++) 
	{ 
		$x=$i;
		for(my $j=1;$j<=$m;$j++)
			{
				print OUT "$x ";
				$x=$x+$n;
			}
		say OUT "0";
	};
for(my $i=1;$i<=$n;$i++)
	{
		for(my $j=$i+1;$j<=$n;$j++)
			{
				for(my $k=1;$k<=$m;$k++)
					{
						$x=$i+($k-1)*$n;
						$y=$j+($k-1)*$n;
						say OUT "-$x -$y 0";
					}
			}
	};
close OUT;


