PSATO - A DISTRIBUTED PROPOSITIONAL PROVER AND ITS APPLICATION TO QUASIGROUP PROBLEMS

We present a distributed/parallel prover for propositional satisfiabil ity (SAT), called PSATO, for networks of workstations. PSATO is based on the sequential SAT prover SATO, which is an efficient implementatio n of the Davis-Putnam algorithm. The master-slave model is used for co mmunication. A simple and effective workload balancing method distribu tes the workload among workstations. A key property of our method is t hat the concurrent processes explore disjoint portions of the search s pace. In this way, we use parallelism without introducing redundant se arch. Our approach provides solutions to the problems of (i) cumulatin g intermediate results of separate runs of reasoning programs; (ii) de signing highly scalable parallel algorithms and (iii) supporting ''fau lt-tolerant'' distributed computing. Several dozens of open problems i n the study of quasigroups have been solved using PSATO. We also show how a useful technique called the cyclic group construction has been c oded in propositional logic. (C) 1996 Academic Press Limited