Parallelization of MGTP 

There are several resources for parallelization of MGTP: 

case splitting 
conjunctive matching in the antecedent part 
subsumption test 


We focused on OR parallelization in case splitting and on AND parallelization 
in conjunctive matching and subsumption test. 

OR Parallelization 

For non-Horn and ground problems, it is sufficient to exploit OR paral-
lelization induced by case splitting. We implemented an OR parallel version 
of MGTP based on the MERC method.

The processor allocation methods we have adopted achieve `bounded-OR' 
parallelization in the sense that OR parallel forking in the proving process is 
suppressed so as to meet restricted resource circumstances. To do this, we 
adopted a scheme, called level restricted allocation. 

We expanded model candidates, starting with an empty model, using a sin-
gle master processor until the number of candidates exceeded the number of 
available processors. We, then, distributed the remaining tasks to slave pro-
cessors. Each slave processor explored the branches assigned without further 
distributing tasks to any other processors. 

This allocation scheme for task distribution works fairly well, since the 
communication cost can be minimized. 





Level restricted allocation


					- 67 -