%%%%%%%%%%%%
% sat(F,I,M)
% si F es satisfactible, M sera el model de F afegit a la interpretació I (a la primera crida I sera buida).
% Assumim invariant que no hi ha literals repetits a les clausules ni la clausula buida inicialment.
sat([],I,I):-     write('SAT!!'),nl,!.
sat(CNF,I,M):-
    % Ha de triar un literal d’una clausula unitaria, si no n’hi ha cap, llavors un literal pendent qualsevol.
    decideix(CNF,Lit),

    % Simplifica la CNF amb el Lit triat (compte pq pot fallar, es a dir si troba la clausula buida fallara i fara backtraking).
    simplif(Lit,CNF,CNFS),
    \+ teLlistaBuida(CNFS),
    append([Lit], I, X),

    % crida recursiva amb la CNF i la interpretacio actualitzada
    sat(CNFS , X ,M).

%%%%%%%%%%%%%%%%%%
% decideix(F, Lit)
% Donat una CNF,
% -> el segon parametre sera un literal de CNF
%  - si hi ha una clausula unitaria sera aquest literal, sino
%  - un qualsevol o el seu negat.
decideix(L1, Y):-agafarElement(L1,L2), esborraDuplicats([L2],A), member(Y, A).

%%%%%%%%%%%%%%%%%%%%%
% agafarElement(L, N)
% Retorna un element de la llista de listes, prioritzant els que es troben sols a una llista
agafarElement(ListOfLists,Element):-
    length(List,_),
    member(List,ListOfLists),
    member(Element,List), !.

%%%%%%%%%%%%%%%%%%%%%%%
% esborraDuplicats(L1, L2)
% L2 és L1 sense els elements duplicats
esborraDuplicats([], []).
esborraDuplicats([H|T], [H|T1]) :-
    esborraElementLlista(H, T, T2),
    esborraDuplicats(T2, T1).

%%%%%%%%%%%%%%%%%%%%%
% simlipf(Lit, F, FS)
% Donat un literal Lit i una CNF,
% -> el tercer parametre sera la CNF que ens han donat simplificada:
%  - sense les clausules que tenen lit
%  - treient -Lit de les clausules on hi es, si apareix la clausula buida fallara.
simplif([], [], _):-!.
simplif(_, [], []):-!.
simplif(X, [Y|Ys], Z):-L is -X, member(L,Y), treu(L, Y, Y2), !, append([Y2], Ys, Y2s), simplif(X, Y2s, Z), !.
simplif(X, [Y|Ys], Z):-member(X,Y), !, simplif(X, Ys, Z), !.
simplif(X, [Y|Ys], Z):-!, simplif(X, Ys, Zs), append([Y], Zs, Z), !.

%%%%%%%%%%%%%%%%
% treu(X,L1,L2)
% L2 es L1 sense X.
treu(_,[],[]).
treu(X,[X|L1],L2):-treu(X,L1,L2).
treu(X,[Y|L1],[Y|L2]):-treu(X,L1,L2).