[mercury-users] re: examples of non-chronological search

[Henk Vandecasteele]

Don Smith wrote:
> 
> Good morning,
> 
> Fergus wrote:
> >I think it would be helpful if someone could give a pointer to one or
> >two examples of constraint-based applications for which chronological
> >backtracking is not appropriate.
> 
> References at end.
> 
> Last time I looked (about a year ago!), two of the fastest methods for
> solving SAT problems were:  walksat and relevance-bounded-learning.
> 
I believe there is nothing wrong with Mercury to implement
GSAT-algorithm based on probabilistic methods. I did it once, as an
exercise. Someone over here implemented the same algorithm
in C, it was not faster. The main-difference was that I didn't have to
debug my program. The compiler did this for me!
The program in attachment. Of course there is much room for 
optimisation with more sophisticated data-structures.
( I can send the data-files to people interested)

Concerning Intelligent backtracking, that seems quite challenging to
implement on top of Mercury!
An application where we used this (maybe quite academic):
Find a pre-interprettion for a logic program, such that a model
exists where the query is false. When such a pre-interprettion
exists we known that SLD-resolution will not find a solution, 
but of course may loop. Such looping programs are our targets!
Using Intelligent Backtracking with Prolog, proved to be faster than
Constraint programming using Forward checking, Lookahead, ... 
and chronologic backtracking. Using probabilistic methods 
might be another way out.

Regards,

Henk
-------------- next part --------------
:- module gsat.

:- interface.

:- import_module io.


:- pred main(io__state::di, io__state::uo) is det.



:- implementation.

:- import_module bimap.
:- import_module list.
:- import_module int.
:- import_module string.
:- import_module bool.
:- import_module array.
:- import_module require.
:- import_module random.
:- import_module non_logical_io.


:- type variable_store == bimap__bimap(int, string).
:- type proposition ---> pos(int) ; neg(int).
:- type formula == list__list(list__list(proposition)).
:- type solution == array__array(bool__bool).
	
main -->
	io__command_line_arguments(Args),
	{( Args = [S1, S2, S3],
	   string__to_int(S2, I1),
	   string__to_int(S3, I2) ->
	   FileName = S1,
	   Restart = I1,
	   Climbs =  I2
	 ;   error("gsat filename restart climb"))},
	io__open_input(FileName, HandleResult),
	( {HandleResult=ok(HandleT) -> Handle = HandleT; error("cannot open")}),
	go_for_it(Handle, Restart, Climbs).

:- pred go_for_it(io__input_stream, int, int, io__state, io__state).
:- mode go_for_it(in, in, in, di, uo).

go_for_it(Handle, Restart, Climb) -->
	read_formula(Handle, Formula, Variables, TotalNumber, Token),
	{random__init(5, Supply),
	 array__init(TotalNumber, bool__no, Solution0),
	 list__length(Formula, FLen),
	 non_logical_io__write_string("length: "),
	 non_logical_io__write_int(FLen),
	 non_logical_io__write_string(" go "),
	 start(Restart, Climb, Formula, Solution0,Solution,FLen,TotalNumber,Supply,0, 0, Restarts, Climbs)},
	io__write_string("restarts: "),
	io__write_int(Restarts),
	io__write_string(" climbs: "),
	io__write_int(Climbs),
	io__write_string("\n"),
	write_solution(Variables, Solution, TotalNumber),
	( {Token = next} ->
	   go_for_it(Handle, Restart, Climb);
	    io__close_input(Handle)
	).


:- pred initial_solution_fill_in(solution, solution, int, int,
				 random__supply,random__supply).
:- mode initial_solution_fill_in(array_di, array_uo, in, in, mdi, muo).

initial_solution_fill_in(Solution0, Solution, Count0, Count, Supply0, Supply):-
	( Count0 = Count ->
	    Solution = Solution0,
	    Supply = Supply0
	;
	    random__random(Res, Supply0, Supply1),
	    N = Res rem 2,
	    (N = 1 -> 
                array__set(Solution0, Count0, yes, Solution1);                
                array__set(Solution0, Count0, no, Solution1)
	    ),
	    Count1 is Count0 +1,
	    initial_solution_fill_in(Solution1, Solution,
				     Count1, Count, Supply1, Supply)
	).

:- pred start(int, int, formula, solution, solution, int, int, supply, int, int, int,int).
:- mode start(in, in, in, array_di, array_uo, in, in, mdi, in, in, out, out) is det.

start(Restart, Climbs, Formula, Solution0, Solution, FLen, Count, Supply0,
      TR0, TC0, TR1, TC1):-
	(  Restart = 0 -> Solution0 = Solution, TR1= TR0, TC1=TC0;
           initial_solution_fill_in(Solution0, Solution1, 
                                    0, Count, Supply0, Supply1),
	   start_climb(Climbs, Formula, Solution1, Solution2, FLen, CountTrue,
                       Supply1, Supply2, TC0, TC2),
	   ( CountTrue = FLen -> 
             non_logical_io__write_string("ok\n"),
	     Solution2 = Solution, TR1= TR0, TC1=TC2;
             non_logical_io__nl,
	     Restart1 is Restart -1,
	       TR2 is TR0 + 1,
	     start(Restart1, Climbs, Formula, Solution2, Solution, FLen, 
                   Count, Supply2, TR2, TC2, TR1, TC1)
           )
	).

:- pred start_climb(int, formula, solution, solution, int, int, supply,supply,
		    int, int).
:- mode start_climb(in, in, array_di, array_uo, in, out, mdi, muo, in, out) is det.

start_climb(Climbs, Formula, Solution0, Solution, FLen, CountTrue, 
            Supply0, Supply, TC0, TC1):-
	check(Formula, Solution0, CountTrue1),
        non_logical_io__write_int(CountTrue1),
        non_logical_io__write_string(" "),
	( CountTrue1 = FLen  ->
	  Supply = Supply0, Solution = Solution0,
	  CountTrue = CountTrue1, TC1 = TC0;
	  ( Climbs = 0 -> 
	    Supply = Supply0, Solution = Solution0, CountTrue = CountTrue1,
	    TC1 = TC0;   
	    climb(Formula, Solution0, Solution1, Supply0, Supply1),
	    Climbs1 is Climbs - 1,
	      TC2 is TC0 +1,
	   start_climb(Climbs1, Formula, Solution1, Solution, FLen, CountTrue, 
                       Supply1,Supply, TC2, TC1)
	  )
	).

:- pred climb(formula, solution, solution, supply, supply).
:- mode climb(in, array_di, array_uo, mdi, muo) is det.

climb(Formula, Solution0, Solution, Supply0, Supply):-
	array__max(Solution0, Bound),
	climb_iter(0, Bound, 0, [], List, Formula, Solution0, Solution1),
	list__length(List, Len),
	random__random(R, Supply0, Supply),
        RR is R rem Len,
	catch(RR, List, Index),
	flip(Index, Solution1, Solution).

:- pred catch(int, list(int), int).
:- mode catch(in, in, out) is det.

catch(_N, [], _):- error("exceeds list").
catch(Index, [Head|Tail], N):-
	( Index = 0 -> N = Head;
	  Index1 is Index-1,
	  catch(Index1, Tail, N)
	).


:- pred flip(int, solution, solution).
:- mode flip(in, array_di, array_uo) is det.

flip(Index, Solution0, Solution):-
	array__lookup(Solution0, Index, Value),
	( Value = no -> 
	  array__set(Solution0, Index, yes, Solution);
	  array__set(Solution0, Index, no, Solution)
	).

:- pred climb_iter(int, int, int, list(int), list(int), formula, 
                   solution, solution).
:- mode climb_iter(in, in, in, in, out, in, array_di, array_uo) is det.

climb_iter(Count, Bound, Max, Yet, Final, Formula, Solution0, Solution):-
	( Count = Bound -> Final = Yet, Solution = Solution0;
 	  flip(Count, Solution0, Solution1),
          check(Formula, Solution1, NumberTrue),
	  ( NumberTrue < Max ->
		Max1 = Max,
                Yet1 = Yet;
	    ( NumberTrue > Max ->
	        Max1 = NumberTrue,
	        Yet1 = [Count]; 
                Max1 = Max,
	        Yet1 = [Count|Yet]
            )
	   ),
          flip(Count, Solution1, Solution2),
	  Count1 is Count +1,
          climb_iter(Count1, Bound, Max1, Yet1, Final, Formula, 
                     Solution2, Solution)
	).

:- pred check(formula, solution, int).
:- mode check(in, array_ui, out) is det.
check([], _Solution, 0).
check([Disj|Formula], Solution, CountTrue):-
	check(Formula, Solution, CountTrue1),
	( check_disj(Disj, Solution) ->
	   CountTrue is CountTrue1 +1;
           CountTrue = CountTrue1
	).

:- pred check_disj(list(proposition), solution).
:- mode check_disj(in, array_ui) is semidet.

check_disj([Prop|Disj], Solution):-
       ( ( Prop = pos(Ref),
          array__lookup(Solution, Ref, Value),
 	  Value = yes;
          Prop = neg(Ref),
	  array__lookup(Solution, Ref, Value),
	  Value = no
	 ) -> true;
	check_disj(Disj, Solution)
       ).

:- pred write_solution(variable_store, solution, int, io__state, io__state).
:- mode write_solution(in, array__array_di, in, di, uo).

write_solution(Vars, Solution, Count) -->
	write_solution1(Vars, Solution, 0, Count),
	io__nl.

:- pred write_solution1(variable_store, solution, int,int, io__state, io__state).
:- mode write_solution1(in, array__array_di, in, in, di, uo).

write_solution1(Vars, Solution, Index, Count) -->
	({Index = Count} -> {true};
	    {array__lookup(Solution, Index, Value),
	    bimap__lookup(Vars, Index, Name)},
	    io__write_string(Name),
	    ({Value = bool__yes} ->io__write_string(": 1 ");io__write_string(": 0 ")),
	    {Index1 is Index +1},
	    write_solution1(Vars, Solution, Index1, Count)
	).

:- pred read_formula(io__input_stream, formula, variable_store, int,read_token,
		     io__state, io__state).
:- mode read_formula(in, out, out, out, out, di, uo) is det.

read_formula(Handle, Formula, Variables, TotalCount, Token) -->
	{bimap__init(EmptyVariables)},
	read_formula(Handle, Formula,
		    EmptyVariables, Variables,
		    0, TotalCount, Token).


:- type read_token ---> eofile;prop(proposition);next;or_t;and_t.

:- pred read_token(io__input_stream, read_token, variable_store,
			 variable_store, int, int, io__state, io__state).
:- mode read_token(in, out, in, out, in, out, di, uo) is det.
			 
read_token(Handle, Result, Vars0, Vars1, Count0, Count1) -->
	io__read_word(Handle, CharListRes),
	(   {CharListRes = error(_), error("unexpected error in file")}
	;   
	    {CharListRes = eof, Result = eofile, Count1 = Count0, Vars1=Vars0}
	;
	    {CharListRes = ok(CharList),
	    string__from_char_list(CharList, TokenName)},
	    (	{(TokenName = "not";TokenName = "next";TokenName = "end";
		 TokenName = "or";TokenName = "and")} ->
	    	(   {TokenName = "not"},
		    read_token(Handle, Result1, Vars0, Vars1, Count0, Count1),
		    {(  Result1=eofile, error("problem in reading proposition")
		     ;	 Result1=next, error("problem in reading proposition")
		     ;	 Result1=or_t, error("problem in reading proposition")
		     ;	 Result1=and_t, error("problem in reading proposition")
		     ;	 Result1 = prop(Info),
			 ( Info = pos(Prop), Result = prop(neg(Prop))
			 ; Info = neg(Prop), Result = prop(pos(Prop))
			 )
		     )}
		;   {TokenName = "next", Result=next, Count1=Count0, Vars1=Vars0}
		;   {TokenName = "end", Result = eofile,Count1=Count0, Vars1=Vars0}
		;   {TokenName = "or", Result = or_t,Count1=Count0, Vars1=Vars0}
		;   {TokenName = "and", Result = and_t,Count1=Count0, Vars1=Vars0}
		)
	    ;	
		{( bimap__search(Vars0, Key, TokenName) ->
		    Result = prop(pos(Key)),
		    Vars1 = Vars0,
		    Count1 = Count0
		;   
		    Count1 is Count0 +1,
		    bimap__set(Vars0, Count0, TokenName, Vars1),
		    Result = prop(pos(Count0))
		)}
	    )
	).
		   

:- pred read_formula(io__input_stream, formula, variable_store, variable_store,
		     int, int, read_token, io__state, io__state).
:- mode read_formula(in, out, in, out, in, out, out, di, uo) is det.

read_formula(Handle,  Formula, Vars0, Vars, Count0, Count, Token) -->
	read_token(Handle, Result, Vars0, Vars1, Count0, Count1),
	(   {Result = prop(Prop)} ->
	    read_token(Handle, Result1, Vars1, Vars2, Count1, Count2),
	    (	{Result1=eofile,
		 Formula = [[Prop]], Vars = Vars2, Count=Count1, Token=Result1}
	    ;	{Result1=next,
		  Formula = [[Prop]], Vars = Vars2, Count=Count1, Token=Result1}
	    ;	{ Result1=or_t},
		read_formula(Handle, Formula1, Vars2, Vars, Count2, Count,Token),
		{( Formula1 = [Head|Tail] -> Formula = [[Prop|Head]|Tail];
		    error("will never occur"))}
	    ;	{ Result1=and_t},
		read_formula(Handle, Formula1, Vars2, Vars, Count2, Count,Token),
		{Formula = [[Prop]|Formula1]}
	    ;	{Result1 = prop(_), error("AND, OR, NEXT or END expected")} 
	    )
	;
	    {error("problem reading input")}
	    
	).