Sudoku with Sat in Prolog LI (2014)

Apunte Español
 Universidad Universidad Politécnica de Cataluña (UPC) Grado Ingeniería Informática - 3º curso Asignatura LI Año del apunte 2014 Páginas 4 Fecha de subida 06/12/2014 Descargas 2 Puntuación media Subido por gbaiona

Vista previa del texto

:-include(sud22).
:-dynamic(varNumber/3).
% symbolicOutput(0). % set to 1 to see symbolic output only; 0 otherwise.
symbolicOutput(0).
numNum(9).
writeClauses:- escriuDonats, atleastOneNumPerNode, atmostOneNumPerNode , atmostOnePerBlock , atmostOnePerFila , atmostOnePerColumna .
escriuDonats:- numNum(K), between(1,K,I), between(1,K,N), between(1,K,I), filled(I,J,N), writeClause([x-I-J-N]), fail.
escriuDonats.
atleastOneNumPerNode:- numNum(K), between(1,K,I), between(1,K,J), findall( x-I-J-N, between(1,K,N), C ), writeClause(C), fail.
atleastOneNumPerNode.
atmostOneNumPerNode:- numNum(K), between(1,K,I), between(1,K,J), between(1,K,N1), between(1,K,N2), (N1 < N2), writeClause( [ \+x-I-J-N1, \+x-I-J-N2 ] ), fail.
atmostOneNumPerNode.
atmostOnePerFila:- numNum(K), between(1,K,I), between(1,K,J1), between(1,K,J2), between(1,K,N), (J1 < J2), writeClause( [ \+x-I-J1-N, \+x-I-J2-N ] ) , fail.
atmostOnePerFila.
atmostOnePerColumna:- numNum(K), between(1,K,J), between(1,K,I1), between(1,K,I2), between(1,K,N), (I1 < I2), writeClause( [ \+x-I1-J-N, \+x-I2-J-N ] ) , fail.
atmostOnePerColumna.
square(I,J):- numNum(K), between(1,K,I), between(1,K,J).
sameblock(I1,J1,I2,J2):- square(I1,J1), square(I2,J2), (I is ((I1-1)//3)), (I is ((I2-1)//3)), (J is ((J11)//3)), (J is ((J2-1)//3)).
atmostOnePerBlock:- numNum(K), sameblock(I1,J1,I2,J2) , between(1,K, N), (I1 =\= I2 , J1 =\= J2 ), writeClause( [ \+x-I1-J1-N, \+x-I2-J2-N ] ), fail.
atmostOnePerBlock.
displaySol([]).
displaySol([Nv|S]):- num2var(Nv,x-I-J-N), write(I), write(' '), write(J), write(' = '), write(N), nl, displaySol(S).
% ========== No need to change the following: ===================================== main:- symbolicOutput(1), !, writeClauses, halt. % escribir bonito, no ejecutar main:- assert(numClauses(0)), assert(numVars(0)), tell(clauses), writeClauses, told, tell(header), writeHeader, told, unix('cat header clauses > infile.cnf'), unix('picosat -v -o model infile.cnf'), unix('cat model'), see(model), readModel(M), seen, displaySol(M), halt.
var2num(T,N):- hash_term(T,Key), varNumber(Key,T,N),!.
var2num(T,N):- retract(numVars(N0)), N is N0+1, assert(numVars(N)), hash_term(T,Key), assert(varNumber(Key,T,N)), assert( num2var(N,T) ), !.
writeHeader:- numVars(N),numClauses(C),write('p cnf '),write(N), write(' '),write(C),nl.
countClause:- retract(numClauses(N)), N1 is N+1, assert(numClauses(N1)),!.
writeClause([]):- symbolicOutput(1),!, nl.
writeClause([]):- countClause, write(0), nl.
writeClause([Lit|C]):- w(Lit), writeClause(C),!.
w( Lit ):- symbolicOutput(1), write(Lit), write(' '),!.
w(\+Var):- var2num(Var,N), write(-), write(N), write(' '),!.
w( Var):- var2num(Var,N), write(N), write(' '),!.
unix(Comando):-shell(Comando),!.
unix(_).