ROO Without Deletion

In this section we present the parallel version of Algorithm 1 and its implementation based on OTTER.

An early attempt to parallelize Algorithm 1 focused on the inner ``for'' loop. This is relatively straightforward, since the rewriting, subsumption, and filtering of one new clause is independent from that of another, as long as one finishes up the loop by checking for subsumption among members of the batch. The problem with this approach is that even when there are large numbers of clauses in each batch, the barrier at the end of the loop meant that many processes were temporarily idle.

The key idea here is to parallelize the outer ``while'' loop instead. That is, we will consider multiple ``given'' clauses simultaneously. This both increases the grain size of the parallel computation and removes any barriers. The difficulty, of course, is that without some care, two copies of the same clause might enter the permanent clause space, each deduced and post-processed by a different process. We will also need to solve technical problems associated with adding clauses to the clause space while it is in use by other clauses.

Our approach is to use an intermediate holding area, which we will call (arbitrarily) K. New clauses are first put in K, form which they are removed by a single process which repeats the post procces of the clause before adding it to the clause database. Thus we break down the work to be done into two tasks: A and B. At any moment multiple processes will be executing task A, but at most one process will be executing task B. Each instance of Task A is associated with a given clause. Task B is only executed when the set K is non-empty,

  

Figure: Flow of Data in Simplified ROO

2#2

  

Figure: Task A

3#3

  

Figure: Task B

4#4

Note that there is not a separate process dedicated to Task B. Rather, we create a uniform pool of processes, each of which performs the loop shown in Figure .

  

Figure: Main loop performed by all processes

5#5

The loop continues until some process detects unit conflict or until the set of support is empty and all processes are waiting for a clause to appear there.