Sudoku Log. 4x4

Logica Computacional: Primera pr`ctica
`
a
L`gica proposicional
o
Grau en Enginyeria Inform`tica
a
Universitat de Lleida
Curs 2012-2013

Mini-sudoku de 4 × 4
Un mini-sudoku de 4 × 4consisteix en una graella de 4 × 4 cel.les (16 caselles) dividida en
subquadr´
ıcules de 2 × 2 (tamb´ anomenades “caixes”o “regions”) amb els valors de l’u al quatre
e
de manera que no es poden repetirels valors dins d’una mateixa fila, columna i subquadr´
ıcula.
La pr`ctica consisteix en codificar en l`gica proposicional el problema de la resoluci´ d’un
a
o
o
mini-sudoku de 4 × 4 i resoldre,mitjan¸ant un solver de Sat, els mini-sudokus seg¨ents i tres
c
u
m´s proposats per vosaltres:
e
3

1

2

2

2

3

1

3

4

4
4

(a)

(b)

1
(c)

Tasques a realitzar1. Codificar el problema de la resoluci´ d’un mini-sudoku de 4 × 4 en l`gica proposicional.
o
o
2. Transformar la codificaci´ obtinguda de l`gica proposicional a FNC.
o
o
3. Transformar lacodificaci´ obtinguda en FNC a format DIMACS.
o
4. Utilitzant el solver picosat resoldre els mini-sudokus (a), (b) i (c). Determinar si tenen
o no soluci´ i si aquesta ´s unica. En cas que tinguin m´ltiplessolucions, indicar com
o
e´
u
s’interpreta una de les solucions.
5. Proposar 1 mini-sudoku de 4 × 4 amb m´ltiples solucions i obtenir totes les possibles
u
solucions utilitzant el solverpicosat. Indicar com s’interpreta una de les solucions.
6. Proposar 1 mini-sudoku de 4 × 4 irresoluble. Verificar amb el picosat que no t´ soluci´.
e
o
7. Proposar 1 mini-sudoku de 4 × 4 amb soluci´unica. Verificar amb el picosat que t´
o´
e
soluci´ unica.
o´

1

Lliurament de la pr`ctica
a
• Heu d’elaborar un document en format PDF que inclogui les respostes a les tasques
descrites a lasecci´ anterior. Heu de presentar un unic arxiu en format PDF.
o
´
• La pr`ctica ´s individual.
a
e
• La pr`ctica s’ha de lliurar via Sakai, a l’apartat d’Activitats.
a
• Data l´
ımit per...