#!/usr/bin/perl -w

print "p cnf 999 12005\n";

print "c If the input is modified, the numbers of variables\n";
print "c and clauses in the line above must be updated.\n";
print "c \n";

print "c Encoding: a number with decimal digits dij means\n";
print "c digit d is in row i, column j.\n";
print "c Numbers with a decimal digit 0 are unused.\n";

print "c \nc --- fixed values ---\nc \n";
print "118 0\n";
print "421 0\n";
print "232 0\n";
print "545 0\n";
print "447 0\n";
print "749 0\n";
print "853 0\n";
print "357 0\n";
print "163 0\n";
print "965 0\n";
print "371 0\n";
print "474 0\n";
print "277 0\n";
print "582 0\n";
print "184 0\n";
print "894 0\n";
print "696 0\n";

print "c \nc --- at least one number per square ---\nc \n";
for ($i = 1 ; $i <= 9 ; $i++) {
  for ($j = 1 ; $j <= 9 ; $j++) {
    print "1$i$j 2$i$j 3$i$j 4$i$j 5$i$j " .
          "6$i$j 7$i$j 8$i$j 9$i$j 0\n";
  }
}

print "c \nc --- at most one number per square ---\nc \n";
for ($i = 1 ; $i <= 9 ; $i++) {
  for ($j = 1 ; $j <= 9 ; $j++) {
    for ($d = 1 ; $d <= 9 ; $d++) {
      for ($d0 = $d+1 ; $d0 <= 9 ; $d0++) {
        print "-$d$i$j -$d0$i$j 0\n";
      }
    }
  }
}

print "c \nc --- every value at least once per row ---\nc \n";
for ($d = 1 ; $d <= 9 ; $d++) {
  for ($i = 1 ; $i <= 9 ; $i++) {
    print "$d${i}1 $d${i}2 $d${i}3 $d${i}4 $d${i}5 " .
          "$d${i}6 $d${i}7 $d${i}8 $d${i}9 0\n";
  }
}

print "c \nc --- every value at least once per column ---\nc \n";
for ($d = 1 ; $d <= 9 ; $d++) {
  for ($j = 1 ; $j <= 9 ; $j++) {
    print "${d}1$j ${d}2$j ${d}3$j ${d}4$j ${d}5$j " .
          "${d}6$j ${d}7$j ${d}8$j ${d}9$j 0\n";
  }
}

print "c \nc --- every value at least once per box ---\nc \n";
for ($d = 1 ; $d <= 9 ; $d++) {
  for ($n = 0 ; $n <= 2 ; $n++) {
    for ($m = 0 ; $m <= 2 ; $m++) {
      print $d . (3*$n+1) . (3*$m+1) . " " .
            $d . (3*$n+1) . (3*$m+2) . " " . 
            $d . (3*$n+1) . (3*$m+3) . " " . 
            $d . (3*$n+2) . (3*$m+1) . " " . 
            $d . (3*$n+2) . (3*$m+2) . " " . 
            $d . (3*$n+2) . (3*$m+3) . " " . 
            $d . (3*$n+3) . (3*$m+1) . " " . 
            $d . (3*$n+3) . (3*$m+2) . " " . 
            $d . (3*$n+3) . (3*$m+3) . " 0\n";
    }
  }
}

print "c \nc --- every value at most once per row ---\nc \n";
for ($d = 1 ; $d <= 9 ; $d++) {
  for ($i = 1 ; $i <= 9 ; $i++) {
    for ($j = 1 ; $j <= 9 ; $j++) {
      for ($j0 = $j+1 ; $j0 <= 9 ; $j0++) {
        print "-$d$i$j -$d$i$j0 0\n";
      }
    }
  }
}

print "c \nc --- every value at most once per column ---\nc \n";
for ($d = 1 ; $d <= 9 ; $d++) {
  for ($j = 1 ; $j <= 9 ; $j++) {
    for ($i = 1 ; $i <= 9 ; $i++) {
      for ($i0 = $i+1 ; $i0 <= 9 ; $i0++) {
        print "-$d$i$j -$d$i0$j 0\n";
      }
    }
  }
}

print "c \nc --- every value at most once per box ---\nc \n";
for ($d = 1 ; $d <= 9 ; $d++) {
  for ($n = 0 ; $n <= 2 ; $n++) {
    for ($m = 0 ; $m <= 2 ; $m++) {
      for ($i = 3*$n+1 ; $i <= 3*$n+3 ; $i++) {
        for ($j = 3*$m+1 ; $j <= 3*$m+3 ; $j++) {
          for ($i0 = $i ; $i0 <= 3*$n+3 ; $i0++) {
            for ($j0 = 3*$m+1 ; $j0 <= 3*$m+3 ; $j0++) {
              if ($i0 > $i || $j0 > $j) {
                print "-$d$i$j -$d$i0$j0 0\n";
              }
            }
          }
        }
      }
    }
  }
}