% Търсим дали дадена формула в конюнктивна нормална форма е изпълнима.
% Формулата се представя като списък от списъци, където подсписъците
% са елементарните дизюнкции.
% Пример: формулата ((┐P)˅Q) ˄ (P˅Q˅(┐R)) ˄(Q˅R) е представена във вида:
% [[n,P,Q],[P,Q,n,R],[Q,R]].

is_var(p).
is_var(q).
is_var(r).
is_var(u).
is_var(v).
is_var(w).


%Помощни предикати за списъци
append([],L2,L2).
append([H|T],L2,[H|L]):-append(T,L2,L).

deleteall(_,[],[]).
deleteall(X,L,L):-not(member(X,L)).
deleteall(X,[X],[]).
deleteall(X,[X|T],R):-deleteall(X,T,R).
deleteall(X,[H|T],[H|R]):-deleteall(X,T,R).

%set([],[]).
%set([H|T],[H|R]):-deleteall(H,T,T1), set(T1,R).

union(A,B,C):-append(A,B,C1), set(C1,C).

insert(X,L,[X|L]).

insert2(X,[],[X]).
insert2(X,[H|T],[H|R]):-insert2(X,T,R).

member(X,[X|_]).
member(X,[_|T]):-member(X,T).

sublist(S,L):-suffix(L1,L), preffix(S,L1).

preffix([],_).
preffix([H|P],[H|T]):-preffix(P,T).

suffix(L,L).
suffix(S,[_|T]):-suffix(S,T).

last([X],X).
last([_|T],X):-last(T,X).

is_list([]).
is_list([_|T]):-is_list(T).

flatten([],[]).
flatten([H|T],[H|R]):-not(is_list(H)), flatten(T,R).
flatten([H|T],R):-flatten(H,FH), flatten(T,FT),append(FH,FT,R).

head([H|_],H).

second([_,X|_],X).

delete_last([_],[]).
delete_last([H|T],[H|R]):-delete_last(T,R).

%Връща елементарна дизюнкция като списък.
subformula([L|_],L).
subformula([_|T],L):-subformula(T,L).

%Връща променлива от елементарна дизюнкция.
choose([X|_],X):-is_var(X).
choose([_|T],X):-choose(T,X).

%Връща истина, ако от М не следва Sub.
not_true(Sub,M):- len(M,R1), len(Sub,R2),R1>=R2, reverse(Sub,Sub1),compare(Sub1,M).


%"Обръща литералите", т.е премахва отрицанията на променливи
%с отрицания и добавя отрицания на променливи без отрицания в
%елементарна дизюнкция.
reverse([],[]).
reverse([H|T],[n,H|T1]):-is_var(H), reverse(T,T1).
reverse([n,H|T],[H|T1]):-is_var(H), reverse(T,T1).

%Намира броя на променливите в списък на елементарна дизюнкция.
len([],0).
len([n,H,d|T],R):-is_var(H), len(T,R1), R is R1+1.
len([H,d|T],R):-is_var(H), len(T,R1), R is R1+1.
len([n,H|T],R):-is_var(H), len(T,R1), R is R1+1.
len([H|T],R):- is_var(H), len(T,R1), R is R1+1.

%Намира броя на променливите и отрицанията в списък на елементарна дизюнкция.
len2([],0).
len2([_|T],R):-len2(T,R1), R is R1+1.

%Връща истина, ако променливите със или без отрицания от Sub
%се срещат по същия начин в M.
compare([H],M):- is_var(H), member(H,M), not(sublist([n,H],M)).
compare([n,H],M):-is_var(H), sublist([n,H],M).
compare([H|T],M):-is_var(H), member(H,M), not(sublist([n,H],M)), compare(T,M).
compare([n,H|T],M):-is_var(H), sublist([n,H],M), compare(T,M).

%Търси в формулта елементарна дизюнкция от вида C˅l (l е променлива
%или отрицание на променлива), в която l не е се среща в М,
%а от М не следва С. Ако намери такъв
%литерал го добавя в МR.
unitprop(Fl,M,MR):-subformula(Fl,Sub), len2(Sub,R), R =:=1,  head(Sub,X), is_var(X),
                   not(member(X,M)), insert2(X,M,MR),!.
unitprop(Fl,M,MR):-subformula(Fl,Sub), len2(Sub,R), R=:=2, head(Sub,X),
                   second(Sub,Y), not(member(Y,M)), not(is_var(X)) ,is_var(Y),
                   insert2(n,M,MR1), insert2(Y,MR1,MR),!.
unitprop(Fl,M,MR):- subformula(Fl,Sub), choose(Sub,X), not(member(X,M)),
                    delete_x(Sub,X,Sub1), not_true(Sub1,M),not(neg(X,Sub)),
		    insert2(X,M,MR),!.
unitprop(Fl,M,MR):- subformula(Fl,Sub), choose(Sub,X), not(member(X,M)),
                    delete_x(Sub,X,Sub1), not_true(Sub1,M),neg(X,Sub),
		    insert2(n,M,MR1), insert2(X,MR1,MR),!.

%Намира дали даден литерал е с отрицание.
neg(X,[n,X|_]):-is_var(X).
neg(X,[_|T]):- is_var(X), neg(X,T).

%Връща в Sub1 дизюнкцита Sub, в която е премахнат променливата Х.
delete_x(Sub,X,Sub1):-is_var(X),not(neg(X,Sub)), deleteall(X,Sub,Sub1).
delete_x(Sub,X,Sub1):-is_var(X),neg(X,Sub), delete_n(X,Sub,Sub2),
                      deleteall(X,Sub2,Sub1).

delete_n(X,[n,X|T],[X|T]):-is_var(X).
delete_n(X,[H|T],[H|T1]):-is_var(X),delete_n(X,T,T1).

%Вкарва в МR произволна променлива, който не се среща в М,
%като премахва отрицанието (ако има такова) и
%добавя знака d.
decide(Fl,M,MR):-subformula(Fl,Sub), choose(Sub,X),
                not(member(X,M)), insert2(X,M,M1),
                insert2(d,M1,MR),!.

%Вкарва в М думата fail, в случай, се М не съдържа букви d
%и съществува дизюнкция С, която не следва от М.
fail_FL(Fl,M):-not(member(d,M)), subformula(Fl, Sub),
              not_true(Sub,M).

%"Връща се назад":
%Ако М е от вида MldN (където l е литерал,
%N не съдържа букви d), и ако от М не следва някоя
%дизюнкция С, то се "изтрива" N от М и се добавя
%отрицание на l, т.е MR = M┐l.
backtrack(Fl,M,MR):-member(d,M),subformula(Fl, Sub),
                    not_true(Sub,M),modify(M,MR).

modify(M,MR):-suffix(N,M),
              not(member(d,N)), cut_suffix(N,M,M1),
              delete_last(M1,M2), last(M2,X),
              delete_last(M2,M3),
              insert2(n,M3,M4),
              insert2(X,M4,MR).




cut_suffix(N,M,S):-preffix(S,M), append(S,N,M).

%Търси модел за формулата Fl.
find_M(_,M,M):- member(fail,M).
find_M(Fl,M,MR):-unitprop(Fl,M,M1),find_M(Fl,M1,MR),!.
find_M(Fl,M,MR):-decide(Fl,M,M1),find_M(Fl,M1,MR),!.
find_M(Fl,M,MR):-fail_FL(Fl,M), insert2(fail,M,M1), find_M(Fl,M1,MR),!.
find_M(Fl,M,MR):-backtrack(Fl,M,M1),find_M(Fl,M1,MR),!.
find_M(_,M,M):-!.

%Ако е намерен модел, го отпечатва.
model([H]):-is_var(H),write(H), write("=1"),nl.
model([n,H]):- is_var(H), write(H), write("=0"),nl.
model([n,H|T]):-is_var(H), write(H),
                write("=0"),nl, model(T).
model([H|T]):-is_var(H), write(H),
           write("=1"),nl,model(T).


%Проверява дали е намерен модел.
is_sat(Fl):-find_M(Fl,[],MR), member(fail,MR),write("Not satisfiable!"),nl.
is_sat(Fl):-find_M(Fl,[],MR), write("Satisfiable!"),nl,
	    deleteall(d,MR,MR1),model(MR1).



%?-is_sat([[n,p,q,r],[p],[n,q,r],[n,q,n,r],[q,r],[q,n,r]]).
%?-is_sat([[n,p,q],[n,r,u],[n,v,n,w],[w,n,v,n,q]]).
%?-is_sat([[p],[q],[p,n,r]]).
%?-is_sat([[n,r],[n,q],[n,p,r],[p,q],[p,n,u],[n,p,n,u]]).
%?-is_sat([[p,n,q],[p,q,n,r],[n,r,n,q],[r,n,q]]).
%?-is_sat([[p],[n,p]]).
%?-is_sat([[p],[q]]).
%?-is_sat([[p,n,q],[q,n,r],[n,r,n,q],[u,n,v]]).