Esercizio encoding SAT

Il file near.pl contiene un'istanza di un problema di map coloring.  E` costituito da uninsieme di fatti

near(A,B)

che rappresentano gli stati confinanti, piu` un fatto

numcol(N)

che indica quanti colori si hanno a disposizione.

Scrivere un programma (in un linguaggio a scelta) che salva su un file mapcol.cnf la conversione in SAT del problema del mapcoloring con gli encoding visti (direct, support e log). Lo si provi con il SAT solver sviluppato nell'esercizio SAT e con MiniSat.

Chi vuole utilizzare ECLiPSe, puo` usare le primitive:

• open(NomeFile,Modo,FileHandler) per aprire un file. Modo puo` essere read o write.
• write(FileHandler,Dato) per scrivere sul file un Dato
• writeln(FileHandler,Dato) per scrivere sul File un Dato e andare a capo
• close(FileHandler)