Resolvendo Sudoku
Faca um programa que usa o Z3 para resolver um sudoku n x m. O programa deve receber n x m na lista de comando. Em seguida, ele deve ler nm valores inteiros, cada valor representando uma entrada do problema. O valor 0 representa uma casa vazia. Valores maiores que zero representam restrições. Os valores sao lidos linha a linha. O programa deve gerar as clausulas em SMT2, executar o z3 e ler o modelo obtido, se satisfazível. Deve então imprimir a solucão em formato inteligível.
Por exemplo, o sudoku 2 x 3 da figura http://4.bp.blogspot.com/-c-Zw8hfwiaU/T3Cq7C414AI/AAAAAAAAA8Y/WK2olcf2ues/s640/Sudoku2.png seria representado da seguinte forma:
solve-sudoku 2 3
3 1 0 0 0 0
0 0 0 0 2 0
1 0 0 4 0 2
0 2 0 5 0 0
0 0 3 1 0 4
4 0 0 0 0 0
O programa pode ser feito em: python, perl, java, C, C++, Pascal, Haskell, SML, Prolog.
O trabalho é individual, mas pode se feito em até três pessoas. Quer dizer, não há problema em discutir e desenvolver o trabalho em grupo, mas cada um deve submeter o seu, que nao pode ser o mesmo arquivo.