read_data(X):-see('E:\\KRR\\input.txt'),read(X),seen.

write_data(X):-tell('E:\\KRR\\output.txt'),write(X),told.

verify_literals(X,Y):-X == n(Y),!.
verify_literals(X,Y):-Y == n(X).

find_negation(Lit, [H|_], 0):-verify_literals(Lit, H),!.
find_negation(Lit, [_|T], N):-find_negation(Lit, T, N_ord), N is N_ord+1.

find_pair_literals([H|_], Clause_2, 0, Poz2):-find_negation(H, Clause_2, Poz2),!.
find_pair_literals([_|T], Clause_2, Poz1, Poz2):-find_pair_literals(T, Clause_2, N, Poz2), Poz1 is N+1.

verify_clause_uniqueness(_,[]):-!.
verify_clause_uniqueness(C_new, [C|T]):-sort(C_new, C_new_sort), sort(C, C_sort), C_new_sort \== C_sort, verify_clause_uniqueness(C_new, T).

delete_nth([_|T], 0, T):-!.
delete_nth([H|T], N, [H|Rez]):-N>0, M is N-1, delete_nth(T,M,Rez).

create_new_clause(C1, C2, Poz1, Poz2, C_new):-delete_nth(C1, Poz1, Rez1), delete_nth(C2, Poz2, Rez2),append(Rez1, Rez2, C_new).
eliminate_duplicates(C, C_new):-sort(C, C_new).
get_new_clause(C1, C2, Poz1, Poz2, C_new):-create_new_clause(C1, C2, Poz1, Poz2, C_NEW),eliminate_duplicates(C_NEW, C_new).


find_pair_clauses([H|_],C, H, Poz1, Poz2):-find_pair_literals(C, H, Poz1, Poz2),!.
find_pair_clauses([_|T],C, Rez, Poz1, Poz2):-find_pair_clauses(T,C,Rez,Poz1,Poz2).


get_resolvent([H|T],Rez):-find_pair_clauses(T, H, C_pair, Poz1, Poz2),
    get_new_clause(H, C_pair, Poz1, Poz2, Rez),
    verify_clause_uniqueness(Rez, [H|T]),!.
get_resolvent([_|T],Rez):-get_resolvent(T,Rez).


find_box([H|_]):-H == [],!.
find_box([_|T]):-find_box(T).



solve(Set, unsatisfiable):-find_box(Set),!.
solve(Set, Rez):-get_resolvent(Set, Resolvent), 
    append(Set,[Resolvent],New_Set),
    solve(New_Set,Rez),!.
solve(_, satisfiable):-!.


resolution:-read_data(X),solve(X,Result),write_data(Result).





verify_clause_for_atom_1([], _):-!.
verify_clause_for_atom_1([H|T],Atom):-H \== Atom, H\== n(Atom),
    verify_clause_for_atom_1(T,Atom).

get_set_1([], _, []):-!.
get_set_1([H|T], Atom, [H|Rez]):-verify_clause_for_atom_1(H,Atom), get_set_1(T,Atom,Rez),!.
get_set_1([_|T], Atom, Rez):-get_set_1(T,Atom,Rez).

clause_no_atom([], _):-!.
clause_no_atom([H|T], Atom):-H \==Atom, clause_no_atom(T, Atom).

clause_with_atom([H|T], Atom, T):-H == Atom,!.
clause_with_atom([H|T], Atom, [H|Rez]):- clause_with_atom(T, Atom, Rez).

get_set_2([], _, []):-!.
get_set_2([H|T], Atom, [H_new|Rez]):-clause_no_atom(H, Atom),
    clause_with_atom(H, n(Atom), H_new),
    get_set_2(T, Atom, Rez),!.
get_set_2([_|T], Atom, Rez):-get_set_2(T, Atom, Rez).

verify_clause_existing([],_):-!.
verify_clause_existing([H|T],C):-sort(H,H_sort),
    sort(C,C_sort), 
    H_sort \== C_sort,
    verify_clause_existing(T,C).

union_sets(Set_1, [], Set_1):-!.
union_sets(Set_1, [H|T], [H| Rez]):-union_sets(Set_1, T, Rez),
    verify_clause_existing(Rez, H),!.
union_sets(Set_1, [_|T], Rez):-union_sets(Set_1, T, Rez).


dot_product(Set, Atom, Rez):-get_set_1(Set, Atom, Set_1),
    get_set_2(Set, Atom, Set_2),
    union_sets(Set_1, Set_2, Rez).

get_set_2_neg([], _, []):-!.
get_set_2_neg([H|T], Atom, [H_new|Rez]):-clause_no_atom(H, n(Atom)), 
    clause_with_atom(H, Atom, H_new), 
    get_set_2_neg(T, Atom, Rez),!.
get_set_2_neg([_|T], Atom, Rez):-get_set_2_neg(T, Atom, Rez).

dot_product_neg(Set, Atom, Rez):-get_set_1(Set, Atom, Set_1), 
    get_set_2_neg(Set, Atom, Set_2), 
    union_sets(Set_1, Set_2, Rez).


get_list_of_terms([], []):-!.
get_list_of_terms([H|T], Rez):-get_list_of_terms(T, Rez_1), 
    append(Rez_1, H, Rez).

eliminate_terms([],[]):-!.
eliminate_terms([H|T],[H|Rez]):-atom(H), eliminate_terms(T, Rez),!.
eliminate_terms([_|T],Rez):-eliminate_terms(T, Rez).

get_list_of_atoms(Set, Rez):-get_list_of_terms(Set, X), eliminate_terms(X, Rez).

get_unique_atoms(List, Rez):-sort(List, Rez).


count_appearances([], _, 0):-!.
count_appearances([H|T], Atom, N):-H == Atom, 
    count_appearances(T, Atom, M), 
    N is M + 1,!.
count_appearances([_|T], Atom, N):-count_appearances(T, Atom, N).


most_frequent_atom([X], Lista, Rez, X):-count_appearances(Lista, X, Rez),!.
most_frequent_atom([H|T], Lista, Max_2, H):-
    most_frequent_atom(T, Lista, Max_1, _), 
    count_appearances(Lista, H, Max_2), 
    Max_1 < Max_2,!.
most_frequent_atom([_|T], Lista, Max_1, Atom_1):-
    most_frequent_atom(T, Lista, Max_1, Atom_1).

get_most_frequent_atom(Set, Atom):-get_list_of_atoms(Set, Rez_1),
    get_unique_atoms(Rez_1, Atoms), 
    most_frequent_atom(Atoms, Rez_1, _, Atom).


most_fewest_atom([X], Lista, Rez, X):-count_appearances(Lista, X, Rez),!.
most_fewest_atom([H|T], Lista, Max_2, H):-
    most_fewest_atom(T, Lista, Max_1, _), 
    count_appearances(Lista, H, Max_2), 
    Max_2 < Max_1,!.
most_fewest_atom([_|T], Lista, Max_1, Atom_1):-
    most_fewest_atom(T, Lista, Max_1, Atom_1).


get_most_fewest_atom(Set, Atom):-get_list_of_atoms(Set, Rez_1),
    get_unique_atoms(Rez_1, Atoms), 
    most_fewest_atom(Atoms, Rez_1, _, Atom).


dp_1([], yes):-!.
dp_1(C, no):-find_box(C),!.
dp_1(C, Answer):-get_most_frequent_atom(C, Atom),
    dot_product(C, Atom, Rez),
    dp_1(Rez, Answer),!.
dp_1(C, Answer):-get_most_frequent_atom(C, Atom),
    dot_product_neg(C, Atom, Rez),
    dp_1(Rez, Answer).


dp_2([], yes):-!.
dp_2(C, no):-find_box(C),!.
dp_2(C, Answer):-get_most_fewest_atom(C, Atom),
    dot_product(C, Atom, Rez),
    dp_2(Rez, Answer),!.
dp_2(C, Answer):-get_most_fewest_atom(C, Atom),
    dot_product_neg(C, Atom, Rez),
    dp_2(Rez, Answer).

dp_met_1:-read_data(X),dp_1(X,Result),write_data(Result).
dp_met_2:-read_data(X),dp_2(X,Result),write_data(Result).