%Помощни неща - преобразования на формули, проверки за тавтология, etc
include("sat-help.pl").
%DPLL алгоритъма
include("dpll.pl").

%Тук са само интерфейсните функции, а именно:

%sat_dpll(F) - преобразува F в КНФ и проверява изпълнимост с DPLL. Подходящо за
%формули, които са в КНФ.

%sat_lazy(F) - проверява изпълнимостта на F като изчерпва всички възможни
%оценки (спира, когато намери две оценки при които F има различна стойност).

%sat_cnf(F) - проверява изпълнимостта на F по следната схема:
%1)Проверява стойността V на F за една произволна оценка.
%2)Ако V=1, проверява дали F е тавтология като я преобразува в КНФ
%2)Ако V=0, проверява дали F е противоречие като преобразува not(F) в КНФ
%Работи много бавно.



sat_dpll(F):-not(is_formula(F)),
  write("Not a valid formula.\n"),!.
sat_dpll(F):-varset(F, V),
  member(X, V),
  not(is_var_dpll(X)),
  write("Formula contains variables, which cannot be used with DPLL.\n"),!.
sat_dpll(F):-cnf(F,R),
  cnf_to_list(R, L),
  list_to_dpll(L, D),
  is_sat(D).


sat_lazy(F):-not(is_formula(F)),
  write("Not a valid formula\n"),!.
sat_lazy(F):-value1(F, V),
  sat_lazy2(F, V).
sat_lazy2(F, 0):-is_contradiction_lazy(F),
  write("contradiction\n"),!.
sat_lazy2(F, 1):-is_tautology_lazy(F),
  write("tautology\n"),!.
sat_lazy2(_, _):-
  write("satisfiable\n").


sat_cnf(F):-not(is_formula(F)),
  write("Not a valid formula.\n"),!.
sat_cnf(F):-value1(F, V), sat_cnf2(F, V).
sat_cnf2(F, 1):-is_tautology(F),
   write("tautology\n"),!.
sat_cnf2(F, 0):-is_contradiction(F),
   write("contradiction\n"),!.
sat_cnf2(_, _):-
  write("satisfiable\n"),!.



%Формулите се представят във вида от дефиницията в sat-help.pl.
%Променливи са p, q, r, u, v, w и списъците от вида [var, X], където X е
%естествено число. 
%Примери:

?-sat_dpll([p, or, [n,p]]).
%?-sat_XXX([p, and, [n,p]]).
%?-sat_XXX([[p,and,q], equ, [n, [[n,p], or, [n,q]] ] ]).
%?-sat_XXX([ [[n,p], equ, q], imp, [r, imp, [u, equ, [v, imp, [n, [p, or,q]]]]]]).


%DPLL алгоритъма работи със вход --- списък от елемендарни дизюнкции, като 
%елементарните дизюнкции са представени като списъци от променливи и 'n'.
%Може да се вика с формули в този формат, без да се налага да се преобразуват 
%със предиката is_sat

%Примери:
%?-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]]).