#!/usr/bin/python
import math
import os
import sys
from sys import stderr
from pprint import pprint

def die(msg):
    stderr.write(msg + "\n")
    sys.exit(1)

def distinctLabel(i, j, size):
    out = []
    out.append([(i, j, k, 1) for k in xrange(1, size+1)])
    for k in xrange(1, size+1):
        for l in xrange(1, size+1):
            if k != l:
                out.append([(i, j, k, -1), (i, j, l, -1)])
    return out

def allDistinctLabels(size):
    out = []
    for i in xrange(size):
        for j in xrange(size):
            out += distinctLabel(i, j, size)
    return out

def rowConstraints(size):
    return [[(i, j) for i in xrange(size)] for j in xrange(size)]

def colConstraints(size):
    return [[(i, j) for j in xrange(size)] for i in xrange(size)]

def squareConstraints(size):
    boxsize = int(math.sqrt(size))
    boxInd = [(i * boxsize, j * boxsize) for i in xrange(boxsize) for j in xrange(boxsize)]
    return [[(boxi + i, boxj + j) for i in xrange(boxsize) for j in xrange(boxsize)] for (boxi, boxj) in boxInd]

def sudokuConstraints(size):
    out = []
    for k in xrange(1, size+1):
        out += [[(i, j, k, 1) for (i, j) in e] for e in rowConstraints(size)]
        out += [[(i, j, k, 1) for (i, j) in e] for e in colConstraints(size)]
        out += [[(i, j, k, 1) for (i, j) in e] for e in squareConstraints(size)]
    return out

def puzzleConstraints(board):
    return [[(i, j, board[i][j], 1)] for i in xrange(len(board)) for j in xrange(len(board[i])) if board[i][j] != 0]


def getCnf(board):
    size = len(board)
    return allDistinctLabels(size) + sudokuConstraints(size) + puzzleConstraints(board)

def tupToInt(tup, size):
    return tup[3] * ((tup[0] * (size ** 2)) + (tup[1] * size) + (tup[2] - 1) + 1)

def intToTup(val, size):
    val -= 1
    val1 = val / (size ** 2)
    val = val % (size ** 2)
    val2 = val / size
    val = val % size
    return (val1, val2, val + 1)

def boardToDimacs(board):
    size = len(board)
    cnf = getCnf(board)
    out = [["p", "cnf", str(tupToInt((size - 1, size - 1, size, 1), size)), str(len(cnf))]]
    for c in cnf:
        out.append([str(tupToInt(e, size)) for e in c] + ["0"])
    return '\n'.join([' '.join(c) for c in out])

def main():
    # Read the filenames from the command line.
    ArgNames = "InPuz OutSol SatExec TempToSat TempFromSat"
    if len(sys.argv) < 6:
        die("Usage: " + sys.argv[0] + " " + ArgNames + "\n")
    filenames = dict(zip(ArgNames.split(), sys.argv[1:]))

    if filenames['SatExec'][:2] != './':
        filenames['SatExec'] = './' + filenames['SatExec']

    # Read the puzzle
    InPuz = open(filenames['InPuz'], "r")
    board = []  # board[r][c] will hold the number in row r, column c.
    size = None
    for line in InPuz:
        if size == None:
          size = int((line.split())[0])
          continue
        board.append([int(x) for x in line.split()])
    bsize = len(board)
    assert size == bsize
    for row in board: assert(len(row) == bsize)
    #pprint(board)

    dimacs = boardToDimacs(board)

    # Write the SAT problem in DIMACS
    TempToSat = open(filenames['TempToSat'], "w")
    TempToSat.write(dimacs)
    TempToSat.close()

    # Execute MiniSAT
    if (os.path.exists(filenames['TempFromSat'])):
        os.system("rm " + filenames['TempFromSat'])
    os.system(
        "bash -c '" +
        " ".join([filenames[x] for x in ['SatExec','TempToSat','TempFromSat']])
        + " &> minisat.log'"
    )

    # Read the solution from MiniSAT
    if (not os.path.exists(filenames['TempFromSat'])):
        print "Error: No output from MiniSAT!"
        os.system("cat minisat.log")
        sys.exit(1)
    TempFromSat = open(filenames['TempFromSat'], "r")
    ans = TempFromSat.readline()
    if (ans != "SAT\n"):
        die("Unsatisfiable: ")
    SolnVals = [int(x) for x in TempFromSat.readline().split()]
    # TODO: Update the board based on the solution generated by MiniSAT.

    boardSol = [intToTup(i, size) for i in SolnVals if i > 0]

    for e in boardSol:
        board[e[0]][e[1]] = e[2]

    # Write the solution
    OutSol = open(filenames['OutSol'], "w")
    for row in board:
        OutSol.write(" ".join(str(x) for x in row) + "\n")
    OutSol.close()

main()

