% Computational Intelligence: a logical approach.
% Prolog Code.
% Finding minimal Conflicts by iterative deepening
% Copyright (c) 1998, Poole, Mackworth, Goebel and Oxford University Press.
% `<-' is the object-level `if'
:- op(1150, xfx, <- ).
% `&' is the object level conjunction.
:- op(950,xfy, &).
% conflict(C) is true if C is a minimal conflict.
conflict(C) :-
iprove(C,0).
% iprove(C,Bnd) is true if we can prove C is a minimal
% conflict using an iterative deepening search,
% starting from bound Bnd. The bound is the number of
% assumptions we can have in an explanation.
:- dynamic(failed/1).
% failed(How) means that the goal failed How the
% previous iteration. How = naturally or unnaturally
iprove(C,Bnd) :-
retractall(failed(_)),
asserta(failed(naturally)),
bhprove(false,Bnd,[],C),
\+ found(C),
assert(confl(C)).
iprove(G,B) :-
failed(unnaturally),
B1 is B+1,
iprove(G,B1).
% bhprove(G,Bound,C1,C2) is true if we can prove
% G given the assumables in C1 resulting in the
% assumables in C2, and never exceeding the Bound
% on the number of assumables.
bhprove(true,_,D,D) :- !.
bhprove((A & B),Bnd,C1,C3) :- !,
bhprove(A,Bnd,C1,C2),
bhprove(B,Bnd,C2,C3).
bhprove(G,Bnd,C1,C2) :-
(G <- Body),
bhprove(Body,Bnd,C1,C2).
bhprove(G,_,C,C) :-
member(G,C).
bhprove(G,Bnd,C,[G|C]) :-
\+ member(G,C),
assumable(G),
length(C,LC),
LC < Bnd.
bhprove(G,Bnd,C,_) :-
\+ member(G,C),
assumable(G),
length(C,LC),
LC >= Bnd,
retract(failed(_)),
assert(failed(unnaturally)),
fail.
% found(C) is true if C has already been found as
% a conflict. It uses the dynamic relation confl(C1)
% to record what conflicts have been found
:- dynamic(confl/1).
found(C) :-
confl(C1),
subset(C1,C).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% The following are standard definitions
% member(X,L) is true if X is a member of list L
member(X,[X|_]).
member(X,[_|L]) :-
member(X,L).
% subset(L1,L2) is true if L1 is a subset of list L2
subset([],_).
subset([A|B],L) :-
member(A,L),
subset(B,L).