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.

PSATO: a distributed propositional prover and its application to quasigroup problems

BONACINA, Maria Paola
;
1996-01-01

Abstract

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.
1996
Satisfiability in propositional logic; SAT; Davis-Putnam-Logemann-Loveland procedure; DPLL; parallelization of; master-slaves architecture
File in questo prodotto:
File Dimensione Formato  
JSC1996psato.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 268.36 kB
Formato Adobe PDF
268.36 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/300534
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 150
  • ???jsp.display-item.citation.isi??? 97
social impact