Path: utzoo!mnetor!uunet!mcvax!prlb2!kulcs!bimbart
From: bimbart@kulcs.uucp (Bart Demoen)
Newsgroups: comp.lang.prolog
Subject: theorem prover of R. Overbeek
Message-ID: <1150@kulcs.UUCP>
Date: 23 Feb 88 08:46:23 GMT
Reply-To: bimbart@kulcs.UUCP (Bart Demoen)
Organization: Katholieke Universiteit Leuven, Dept. Computer Science
Lines: 160

I have been busy with the theorem prover of R. Overbeek, which was used
as a benchmarking program and a challenge to the prolog community. I want
to report here on my experiences with changing the program, introducing
destructive assignment and finding a reason why his prolog program is 20
times slower than his C program for this problem.

The unchanged version of the program took 77 sec in BIMprolog, on a SUN3/50
with the boys example (it is slow, I know, the main reason is that the bit
operations on integers are not yet in assembler, they are interpreted now;
and if you try to make time measurements, you will notice how much time the
program spends in get_next_literal and get_literals)

The first change I made to the program, was to replace the definition of
num_lits/3:

	num_lits(_p,_n,_num) :- c(_p,0,_m) , c(_n,_m,_num) .

	c(0,_i,_i) :- ! .
	c(_n,_i,_j) :- _k is _n / 2 ,
			_i1 is _i + _n - 2 * _k ,
			c(_k,_i1,_j) .

This reduced the runtime to 70 seconds !

By giving another prolog definition to get_next_literal and get_literals, I
gained another 22 seconds ! (I am a bit ashamed about this prolog definition,
so I will not distribute it over the net, but you can obtain it from me
privatly)

Some small changes involved:

	the test for tautology before the test for forward_subsumed
		(that's how it is in C !)

	form_resolvent/7 is symmetric in the first 2 argument pairs (at least
	that's the way it is used) so there is no need to have 2 definitions
	of form_resolvent/8; accordingly the definition of form_resolvent/7
	becomes

		form_resolvent(Par1Pos,Par1Neg,Par2Pos,Par2Neg,
          	     	ClashLit,ResPosWord,ResNegWord) :-
			Mask is \(1 << (ClashLit - 1)),
     			ResPosWord is ((Par1Pos \/ Par2Pos) /\ Mask ),
      			ResNegWord is ((Par2Neg \/ Par1Neg) /\ Mask).
	(it looks so in C !)

This gained only 1 second.

Then, I replaced all if-then-else constructions by their equivalent with
disjunction and cut: for instance:

	delete_from_database_clauses([Id|Rest],L,Db,NewDb) :-
        (   member(Id,L) ->
                delete_from_database_clauses(Rest,L,Db,NewDb)
        ;   /* otherwise -> */
                delete_from_database(Db,Id,Db1),
                delete_from_database_clauses(Rest,[Id|L],Db1,NewDb)
        ).

became:

	delete_from_database_clauses([Id|Rest],L,Db,NewDb) :-
        (   member(Id,L) , ! ,
                delete_from_database_clauses(Rest,L,Db,NewDb)
        ;   /* otherwise -> */
                delete_from_database(Db,Id,Db1),
                delete_from_database_clauses(Rest,[Id|L],Db1,NewDb)
        ).

Gain: 4 seconds.

The program took now about 44 seconds.

Then, I introduced destructive assignment into the program, as much as possible
without changing the algorithm. So, argrep/4 and delete/3 and
form_updated_index/4 were rewritten with destructive assignment and time
dropped from 44 to 22 seconds.
Actually, there was a small problem with destructive assignment, because at
one place in the program, the old database is used after the new one has been
constructed:

subsume_and_add(Db,ResPos,ResNeg,Parents,NewDb,DelList,NewEnd) :-
        ( (forward_subsumed(Db,ResPos,ResNeg) ; tautology(ResPos,ResNeg) ) ->
                NewDb = Db,
                NewEnd = DelList
        ;   /* otherwise -> */
                add_to_sos(Db,clause(Parents,ResPos,ResNeg),NewDb,NewId),
                write_added_mesg(NewId,clause(Parents,ResPos,ResNeg)),
                back_subsumption(Db,NewId,ResPos,ResNeg,DelList,NewEnd)
        ).                       ^^
                                 ||

In the call to back_subsumption, the first argument can be NewDb, but then in
the second definition of backsub/6, after the call to subsumes/4, an extra test

			Id =\= SubId

must be added. (the C code also shows this test)

For destructive assignment, I implemented (in the BIMprolog kernel of course) a
predicate

	replaca/3 	arg1 : a compound term
			arg2 : an integer between 1 and the arity of arg1
			arg3 : anything

		effect : in arg1, the arg2'th argument is replaced by arg3

and then changed the program accordingly; for instance: the new definiton of
argrep/4:

	argrep(N,Old,Value,Old) :- replaca(Old,N,Value) .


For a destructive delete/2, I had to do something similar.

It is clear that destructive assignment improved the speed, but still the prolog
program is slower by a factor at least 10 than the C version.
With destructive assignment, the program needed 2.5 times less heap.

Not only the lack of destructive assignment is the performance killer in this
program: let's look at a typical sequence in the prolog program and compare it
with the C version:

backsub(...)
        :-
        (   subsumes(SubsumerPos,SubsumerNeg,Pos,Neg) , Id =\= SubId , ! ,
                write_subsumed_mesg(Id,SubId),
                add_element(DelList,Id,EndList)
        ;
                EndList = DelList
        ),
        backsub(...).


    for (pt = lst->next_avl - 1; pt >= lst->first; pt--)
    {
        if ((formula_id != (*pt)->id) && Subsumes(cl,(*pt)))
        {
            printf("clause %d subsumes %d \n", formula_id,(*pt)->id);
            add_to_deleted_list((*pt)->id);
        }
    }

Most prologs recognise tailrecursion and can compile it to iteration, all right.
But, instead of C's if-then-else, prolog creates a choicepoint, makes the test
subsumes/4 (which is an out-of-line call while Subsumes in C is a macro) and
either calls a general procedure to fail, or continues and executes a cut: the
prolog overhead is at least a factor of 50 compared to C ! It is almost a
surprise that prolog is only 20 times slower !
Moreover, the datastructure used in the C and prolog program for sets, (a bit
string, i.e. an integer) is very much in favour of C: in a 'typed' prolog were
dereferencing would not be needed, arithmetic could approach the speed of
C arithmetic, but not in untyped prolog.
Since prolog compiler technology is still immature, the introduction of
destructive assignment improved the speed of the program with only a factor
of 2 (from 44 to 22 seconds) which is not much; but perhaps, in a couple of
years, when we will have implemented all beautiful ideas floating around right
now, the improvement will be from 24 to 2 seconds, making destructive assignment
well worth the effort !