Sudoku with Sat in Prolog (2014)

Ejercicio Inglés
 Universidad Universidad Politécnica de Cataluña (UPC) Grado Ingeniería Informática - 3º curso Asignatura Logica informàtica LI Año del apunte 2014 Páginas 4 Fecha de subida 27/08/2014 Descargas 1 Puntuación media Subido por kaito

Descripción

Program in Prolog from LI that solves a sudoku with prolog using a satsolver

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(_).
readModel(L):- get_code(Char), readWord(Char,W), readModel(L1), addIfPositiveInt(W,L1,L),!.
readModel([]).
addIfPositiveInt(W,L,[N|L]):- W = [C|_], between(48,57,C), number_codes(N,W), N>0, !.
addIfPositiveInt(_,L,L).
readWord(99,W):- repeat, get_code(Ch), member(Ch,[-1,10]), !, get_code(Ch1), readWord(Ch1,W),!.
readWord(-1,_):-!, fail. %end of file readWord(C,[]):- member(C,[10,32]), !. % newline or white space marks end of word readWord(Char,[Char|W]):- get_code(Char1), readWord(Char1,W), !.
%============================================================================ ============ ...