Using hundreds of workstations to solve first-order logic problems
Alberto M. Segre, David B. Sturgill · 1994
This paper describes a distributed, adaptive, first-order logic engine with exceptional performance characteris-tics. The system combines serial search reduction tech-niques such as bounded-overhead subgoal caching and intelligent backtracking with a novel parallelization strategy particularly well-suited to coarse-grained paral-lel execution on a network of workstations. We present empirical results that demonstrate our system’s perfor-mance using 100 workstations on over 1400 first-order logic problems drawn from the “Thousands of Prob-lems for Theorem Provers ” collection. utroduction We have developed an distributed, adaptive, first-order logic engine as the core of a planning system intended to solve