PSATO: A distributed propositional prover and its application to quasigroup problems
PSATO: A distributed propositional prover and its application to quasigroup problems
复制标题
DOI：
10.1006/jsco.1996.0030
复制
发表时间：
1996-04-01
影响因子：
0.7
通讯作者：
Hsiang, J
中科院分区：
文献类型：
--
作者：
Zhang, HT;Bonacina, MP;Hsiang, J
我们为工作站网络提供了一个分布式/并行的命题可满足性（SAT）证明器，称为PSATO。PSATO基于顺序SAT证明器SATO，SATO是Davis-Putnam算法的有效实现。通信采用主从模式。一种简单而有效的工作负载平衡方法在工作站之间分配工作负载。我们的方法的一个关键属性是，并发进程探索搜索空间的不相交部分。通过这种方式，我们使用并行性而不引入冗余搜索。我们的方法提供了解决方案的问题（i）累积中间结果的独立运行的推理程序;（ii）设计高度可扩展的并行算法和（iii）支持“容错”的分布式计算。用PSATO解决了拟群研究中的几十个公开问题。我们还展示了如何一个有用的技术称为循环组建设已编码命题逻辑。(C)1996年学术出版社
We present a distributed/parallel prover for propositional satisfiability (SAT), called PSATO, for networks of workstations. PSATO is based on the sequential SAT prover SATO, which is an efficient implementation of the Davis-Putnam algorithm. The master-slave model is used for communication. A simple and effective workload balancing method distributes the workload among workstations. A key property of our method is that the concurrent processes explore disjoint portions of the search space. In this way, we use parallelism without introducing redundant search. Our approach provides solutions to the problems of (i) cumulating intermediate results of separate runs of reasoning programs; (ii) designing highly scalable parallel algorithms and (iii) supporting ''fault-tolerant'' distributed computing. Several dozens of open problems in the study of quasigroups have been solved using PSATO. We also show how a useful technique called the cyclic group construction has been coded in propositional logic. (C) 1996 Academic Press Limited