1 #!/usr/bin/env perl
   2 
   3 $m=shift;
   4 $n=shift;
   5 
   6 $m > 0 and $n > 0 or die "Usage: $0 m n\n";
   7 @formula=();
   8 
   9 # So: xi,j,k ~ (k-1)*n*n + (j-1)*n+i
  10 
  11 for($k=1; $k <= $m; $k++) {
  12   @clause=();
  13   for($i=1; $i <= $n; $i++) {
  14     for($j=1; $j <= $n; $j++) {
  15       push(@clause, ($k-1)*$n*$n + ($j-1)*$n+$i);
  16     }
  17   }
  18   push(@formula,join(" ",@clause) . " 0");
  19 }
  20 
  21 
  22 for($i=1; $i <= $n; $i++) {
  23   for($j=1; $j <= $n; $j++) {
  24     for($k=1; $k <= $m; $k++) { 
  25       for($l=1; $l <= $m; $l++) { 
  26         if($k != $l) {
  27           push(@formula,sprintf("-%d -%d 0",
  28                  ($k-1)*$n*$n + ($j-1)*$n+$i ,
  29                  ($l-1)*$n*$n + ($j-1)*$n+$i));
  30         }
  31       }
  32     }
  33   }
  34 }
  35 
  36 for($i=1; $i <= $n; $i++) {      
  37   for($j=1; $j <= $n; $j++) {    
  38     for($k=1; $k <= $m; $k++) {
  39       for($l=1; $l <= $n; $l++) {  
  40         for($h=1; $h <= $n; $h++) {  
  41           if(!($l==$i && $h==$j)) {
  42             push(@formula,sprintf("-%d -%d 0", 
  43                  ($k-1)*$n*$n + ($j-1)*$n+$i , 
  44                  ($k-1)*$n*$n + ($h-1)*$n+$l));
  45           }
  46         }
  47       }
  48     }
  49   }
  50 }
  51 
  52 for($i=1; $i <= $n; $i++) {
  53   for($j=1; $j <= $n; $j++) {
  54     for($k=1; $k <= $m; $k++) {
  55       for($l=1; $l <= $n; $l++) {
  56         for($h=1; $h <= $m; $h++) {
  57           if(!($l==$i && $h==$k)) {
  58             push(@formula,sprintf("-%d -%d 0", 
  59                  ($k-1)*$n*$n + ($j-1)*$n+$i , 
  60                  ($h-1)*$n*$n + ($j-1)*$n+$l));
  61           }
  62         }
  63       }
  64     }
  65   }
  66 }
  67 
  68 for($i=1; $i <= $n; $i++) {
  69   for($j=1; $j <= $n; $j++) {
  70     for($k=1; $k <= $m; $k++) {
  71       for($l=1; $l <= $n; $l++) {
  72         for($h=1; $h <= $m; $h++) {
  73           if(!($l==$j && $h==$k)) {
  74             push(@formula,sprintf("-%d -%d 0",
  75                  ($k-1)*$n*$n + ($j-1)*$n+$i ,
  76                  ($h-1)*$n*$n + ($l-1)*$n+$i));
  77           }                  
  78         }
  79       }
  80     }
  81   }
  82 }
  83 
  84 for($i=1; $i <= $n; $i++) {
  85   for($j=1; $j <= $n; $j++) {
  86     for($k=1; $k <= $m; $k++) {
  87       $diff=$i - $j;
  88       for($l=1; $l <= $n; $l++) {
  89         $ll = $l - $diff;
  90         if( $ll > 0 && $ll <= $n ) {
  91           for($h=1; $h <= $m; $h++) {
  92             if(!($l==$i && $ll==$j)) {
  93               push(@formula,sprintf("-%d -%d 0",
  94                  ($k-1)*$n*$n + ($j-1)*$n+$i ,
  95                  ($h-1)*$n*$n + ($ll-1)*$n+$l));
  96             }
  97           }
  98         }
  99       }
 100     }
 101   }
 102 }
 103 
 104 for($i=1; $i <= $n; $i++) {
 105   for($j=1; $j <= $n; $j++) {
 106     for($k=1; $k <= $m; $k++) {
 107       $sum=$i + $j;
 108       for($l=1; $l <= $n; $l++) {
 109         $ll = $sum - $l;
 110         if( $ll > 0 && $ll <= $n ) {
 111           for($h=1; $h <= $m; $h++) {
 112             if(!($l==$i && $ll==$j)) {
 113               push(@formula,sprintf("-%d -%d 0",
 114                  ($k-1)*$n*$n + ($j-1)*$n+$i ,
 115                  ($h-1)*$n*$n + ($ll-1)*$n+$l));
 116             }
 117           }
 118         }
 119       }
 120     }
 121   }
 122 }
 123 
 124 
 125 printf("p cnf %d %d\n",$m*$n*$n,$#formula+1);
 126 foreach (@formula)
 127   {
 128   print "$_\n";
 129   }