
% File: gbj.pl
% Author: Peter Clark
% Purpose: Generalised backjumping -- our improvement on Gaschnig's algorithm
% Date: Dec 1991, tidied July 1992

/*
To execute this with LPE, do the following:
	% prolog
	| ?- compile(cities).		% or compile(zebras)
	| ?- compile(gbj).		% compile the GBJ CSP algorithm + LPE
	| ?- gbj.			% run
*/

:- ensure_loaded(['../lpe','../utils']).

:- nl, nl, write('Type `| ?- gbj.'' to start!'), nl, nl.

gbj :-
	ensure_loaded_gbj,
	ensure_loaded_domain_theory,
	
	reset_counter('hypotheses tried'),
	write('Learning mode (`lpe.'', `pe.'', `ebg.'', `none.'')? '),
	read(Mode),
	set_learning_mode(Mode),

        write('(Re)initialise? (will delete previously learned operational'),
	write(' defns)'), nl, 
	write('               Option (`y.'' or `n.'')? '),
	read(Initialise),

	no_of_generators(N),
	length(Soln, N),
	first_gen_to_apply(GNo),

	% ---------- RUN THE CSP ALGORITHM ----------
	statistics(runtime, _),
	( Initialise = y -> lpe_setup( fails/3 ) ; true ),
	gbj(GNo, [], Soln, X),
	statistics(runtime, [_,Time]),
	% -------------------------------------------

        nl, nl,write(Time), write(' msec CPU time'), nl,
	counter('hypotheses tried', C),
	write('Total number of hypotheses tried: '), write(C), nl, 

	( X = finished 
		-> write('SOLVED!! Solution '), write(Soln), nl, nl,
		   write('More solutions (`y.'' or `n.'')? '), read(n)
		;  write('NO (MORE) SOLUTIONS!!'), nl, nl ).

ensure_loaded_gbj :-			% Ensure correct quality measure loaded
	source_file(quality(_,_), F),
	atom_chars(F, FCh), 
	myappend(_, "gbj.pl", FCh), 
	!.
ensure_loaded_gbj :- 
	compile(gbj).

ensure_loaded_domain_theory :-
	source_file(fails(_,_,_), _), !.
ensure_loaded_domain_theory :-
	write('Hey! You must load a domain theory (`compile(cities).'''),
	write(' or `compile(zebras).'')'), nl,
	write('first, before you can run the CSA!'), nl, nl, 
	fail.

% ---- The Global Backjumping Constraint Satisfaction Algorithm -----

gbj(GNo, GsUsed, Soln, InvolvedGs) :-				% [10]
	all_vals(GNo, GVals),
	gbj(GVals, GsUsed, Soln, GNo, [], InvolvedGs).

gbj([], _, _, _, Involved, Involved).				% [1]
gbj([GVal|GVals], GsUsed, Soln, GNo, ISoFar, I) :-
	next_gen_to_apply(GNo, NextGNo),			% [4]
	!,
	copy(Soln, SolnCopy),
	nmemberchk(GVal, SolnCopy, GNo),
	gbj(NextGNo, [GNo|GsUsed], SolnCopy, IGs),		% [5]
	try_next_val(IGs, SolnCopy, GVals, GsUsed, Soln, GNo, ISoFar, I).
gbj([GVal|GVals], GsUsed, Soln, GNo, ISoFar, I) :-
	copy(Soln, SolnCopy),
	nmemberchk(GVal, SolnCopy, GNo),
	count_hypotheses([GNo|GsUsed], SolnCopy),
	lpe_call( fails(SolnCopy,IGs,_) ),         % ***** LPE ******
	!,
	try_next_val(IGs, SolnCopy, GVals, GsUsed, Soln, GNo, ISoFar, I).
gbj([GVal|_], _, Soln, GNo, _, finished) :- 			% [8]
	nmember(GVal, Soln, GNo).
gbj([_|GVals], _, Soln, GNo, _, ToBlame) :-			% [9]
	ordered_generators(AllGens),
	gbj(GVals, _, Soln, GNo, AllGens, ToBlame).

try_next_val(IGs, _, GVals, GsUsed, Soln, GNo, ISoFar, I) :-
	memberchk(GNo, IGs), !,					% [6]
	union(ISoFar, IGs, NewI),
	gbj(GVals, GsUsed, Soln, GNo, NewI, I).
try_next_val(IGs, Soln, _, _, Soln, _, _, IGs).   		% [7]

first_gen_to_apply(N) :- ordered_generators([N|_]).

next_gen_to_apply(GNo, NextGNo) :-
	ordered_generators(AllGs),
	append([_,[GNo,NextGNo],_], AllGs).

% ======================================================================

count_hypotheses(GsUsed, Soln) :-
	make_a_count('hypotheses tried'),
	counter('hypotheses tried', Ct),
	print_at_intervals(P),
	Ct is integer(Ct/P)*P,
	!,
	nl, write('Hypo number '),
	write(Ct), write(': '), print_bits(GsUsed, Soln), nl.
count_hypotheses(_, _).

print_at_intervals(100).

print_bits([], _).
print_bits([N|Ns], Soln) :-
	print_bits(Ns, Soln),
	nmember(Item, Soln, N),
	write(Item).

% --------------------

:- dynamic counter/2.

reset_counter(C) :- retractall(counter(C,_) ).

make_a_count(Test) :- make_a_count(Test, _).

make_a_count(Test, NewN) :- 
	retract( counter(Test,N) ), !,
	NewN is N + 1, assertz( counter(Test,NewN) ).
make_a_count(Test, 1) :- assertz( counter(Test,1) ).

% ======================================================================
% Definition of `better solution' for constraint satisfaction problems:

:- no_style_check(multiple).

quality(Defn, Q) :-
	Defn = ( fails(_,VarsInvolved,_) :- _),
	remove_tail_var(VarsInvolved),
	sort(VarsInvolved, EarliestToLatest),
	reverse(EarliestToLatest, Q).	

remove_tail_var(X) :- myappend(X, [], _), !. % trick to make X=[a|_] -> X=[a]

reverse(List, Reversed) :-
	reverse(List, [], Reversed).

reverse([], Reversed, Reversed).
reverse([Head|Tail], Sofar, Reversed) :-
	reverse(Tail, [Head|Sofar], Reversed).

:- style_check(multiple).