#!/usr/bin/perl
use strict;
my $puzzleFile = $ARGV[0];
my $satFile = "$puzzleFile.cnf";
open(PUZZLE, "$ARGV[0]");
open(SATFILE, ">$satFile");

my @puzzle = <PUZZLE>;
close(PUZZLE);
my @cells;

my $literalCounter = 0;

my $descriptor = $puzzle[1];

for my $i (1..9) {
  for my $j (1..9) {
    for my $k (1..9) {
      $cells[$i][$j][$k] = &getLiteral();
    }
  }
}

my @board;
for my $row (1..9) {
  my @line = split('',$puzzle[$row]);
  for my $column (1..9) {
    my $cell = $line[$column - 1];
    if ($cell =~ /[0-9]/) {
      for my $value (1..9) {
	if ($value != $cell) {
	  print(SATFILE "-");
	}
	my $literal = $cells[$row][$column][$value];
	print(SATFILE "$literal 0 \n");
      }
    }
  }
}
   
#uniquenessConstraints
for my $row (1..9) {
  for my $column (1..9) {
    for my $value1 (1..9) {
      for my $value2 (($value1 + 1)..9) {
	my $cellValue1 = $cells[$row][$column][$value1];
	my $cellValue2 = $cells[$row][$column][$value2];
	print(SATFILE "-$cellValue1 -$cellValue2 0 \n");
      }
    }
  }
}
					 

#rowConstraints
for my $row (1..9) {
  for my $value (1..9) {
    for my $column (1..9) {
      my $currentCell = $cells[$row][$column][$value];
      print(SATFILE "$currentCell ");
    }
    print(SATFILE "0\n");
  }
}

#columnConstraints
for my $column (1..9) {
  for my $value (1..9) {
    for my $row (1..9) {
      my $currentCell = $cells[$row][$column][$value];
      print(SATFILE "$currentCell ");
    }
    print(SATFILE "0\n");
  }
}

#cellConstraints
for my $bigRow (0..2) {
  for my $bigColumn (0..2) {
    my $baseRow = $bigRow * 3;
    my $baseColumn = $bigColumn * 3;
    for my $value (1..9) {
      for my $littleRow (1..3) {
	for my $littleColumn (1..3) {
	  my $currentCellValue = $cells[$baseRow + $littleRow][$baseColumn + $littleColumn][$value];
	  print(SATFILE "$currentCellValue ");
	}
      }
      print(SATFILE "0 \n");
    }
  }
}



close(SATFILE);
  

sub getLiteral {
  $literalCounter = $literalCounter + 1;
}