Solving the hard Satisfiability Problem is time consuming even for modest-sized problem instances. Solving the Random L-SAT Problem is especially difficult due to the ratio of clauses to variables. This report presents a practical approach to solving the Random L-SAT Problem on a large-scale distributed-memory multiprocessor. In particular, we use a parallel synchronous simulated annealing procedure, called Generalized Speculative Computation, which guarantees the same decision sequence as sequential simulated annealing. We have selected problem instances varying in size from 100-variable/425-clause to 5000-variable/21,250-clause. Experimental results on the AP1000 distributed-memory multiprocessor indicate that Generalized Speculative Computation of synchronous simulated annealing can satisfy 99.9% of the clauses while giving almost a 70-fold speedup on 500 processors.
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- Hardware and Architecture
- Computer Networks and Communications
- Artificial Intelligence