% assignment 2 model solution 2004/5
:- use_module(library(lists)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% resolve(+Set)
%
% derives any contradictions in the set of clauses in Set, which are
% in conjunctive normal form
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
resolve(Set) :-
%  write('Resolving '),write(Set),nl,
  selectpair(Set,Clause1,Clause2),    % select a potential pair for resolving
  process(Set,Clause1,Clause2).       % resolve them or backtrack
resolve(_) :- write('No contradiction derived'),nl.


%%%%%%%%%%%%%%%%
% selectpair(+Set,-Clause1,-Clause2)
%
% selects 2 clauses from Set in a way that all pairs are generated only
% once and Clause1 \= Clause2
%%%%%%%%%%%%%%%%
selectpair([Clause1|Rest],Clause1,Clause2) :-
  member(Clause2,Rest).
selectpair([_|Rest],Clause1,Clause2) :-
  selectpair(Rest,Clause1,Clause2).


%%%%%%%%%%%%%%%%
% process(+Set,+Clause1,+Clause2)
% 
% resolve clauses Clause1 and Clause2, adding result to Set
% several cases to consider: 
%  1) 2 contradicting clauses already exist, so exit.
%  2) derived clause already exist or is subsumed by an existing clause
%  3) derived clause is a tautology (ignored)
%%%%%%%%%%%%%%%%
process(_,[X],[not(X)]) :- write('Contradiction derived'),nl,!. %contradiction?
process(_,[not(X)],[X]) :- write('Contradiction derived'),nl,!. %contradiction?
process(Set,Clause1,Clause2) :-
  resolveclause(Clause1,Clause2,Var,Result),    % resolve 2 clauses if possible
  newclause(Result,Set),                        % require clause to be new
  Result \= [],                                 % require clause to exist
%  write('  Eliminating '),write(Var),write(' in clauses '),
%  write(Clause1),write(' & '),write(Clause2),
%  write(' to get '),write(Result),nl,
  resolve([Result|Set]).                        % recurse on extended set


%%%%%%%%%%%%%%%%
% newclause(+Clause,+Set)
%
% ensures that Clause doesn't already appear in Set, and
% that Clause is not subsumed by any member in Set.
% Attention needed since the terms in a clause can be in different orders.
%%%%%%%%%%%%%%%%
newclause(_,[]).
newclause(Clause,[H|_]) :-
  permutation(Clause,L),sublist(H,L),!,fail.
newclause(Clause,[_|Rest]) :- newclause(Clause,Rest).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% resolveclause(+Clause1,+Clause2,-Var,-Result)
%
% attempts to resolve Clause1 and Clause2, using variable Var and
% producing the result Result. It needs to remove any duplicates
% found in the result, and also return [] if Result is a tautology
% (ie. contains p and ¬p)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
resolveclause(Clause1,Clause2,Var,Result) :-
  findvar(Clause1,Clause2,Var,Rest1,Rest2),  % find a candidate variable
  append(Rest1,Rest2,Merged),                % apend remainders
  remove_duplicates(Merged,CleanMerged),     % remove duplicates
  tautology(CleanMerged,Result).             % check for tautology


%%%%%%%%%%%%%%%%
% findvar(+Clause1,+Clause2,-Var,-Rest1,-Rest2)
%
% Finds some variable Var that appears in Clause1 and Clause2
% as Var and not(Var) or vice versa.
%%%%%%%%%%%%%%%%
findvar(Clause1,Clause2,Var,Rest1,Rest2) :-
  select(Var,Clause1,Rest1),
  select(not(Var),Clause2,Rest2).
findvar(Clause1,Clause2,Var,Rest1,Rest2) :-
  select(not(Var),Clause1,Rest1),
  select(Var,Clause2,Rest2).


%%%%%%%%%%%%%%%%
% tautology(+Set,-Result)
%
% Returns Result=[] if Set contains Var and not(Var), otherwise
% does nothing
%%%%%%%%%%%%%%%%
tautology(Set,[]) :-
  member(Item,Set),
  member(not(Item),Set),!.
tautology(Set,Set).
