Using Hundreds of Workstations to Solve First-Order Logic Problems

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 12

Automated Reasoning

This paper describes a distributed, adaptive, first-order logic engine with exceptional performance characteristics. The system combines serial search reduction techniques such as bounded-overhead subgoal caching and intelligent backtracking with a novel parallelization strategy particularly well-suited to coarse-grained parallel execution on a network of workstations. We present empirical results that demonstrate our system’s performance using 100 workstations on over 1400 first-order logic problems drawn from the "Thousands of Problems for Theorem Provers" collection.