Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(11)
Concurrent Process
cumulant
Cyclic Group
Distributed Computing
Efficient Implementation
Network of Workstation
Parallel Algorithm
Propositional Logic
Propositional Satisfiability
Search Space
Davis Putnam
Related Publications
(17)
Implementing the DavisPutnam Method
A Machine Program for Theorem Proving
A Computing Procedure for Quantification Theory
A Fast Parallel SATSolver  Efficient Workload Balancing
Multiprocessing of Combinatorial Search Problems
Subscribe
Academic
Publications
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems,10.1006/jsco.1996.0030,Journal of Symbolic Computation,Hantao Zha
Edit
PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems
(
Citations: 97
)
BibTex

RIS

RefWorks
Download
Hantao Zhang
,
Maria Paola Bonacina
,
Jieh Hsiang
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 DavisPutnam 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 rea soning programs; (ii) designing highly scalable parallel algorithms and (iii) supporting "faulttolerant" 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.
Journal:
Journal of Symbolic Computation  JSC
, vol. 21, no. 4, pp. 543560, 1996
DOI:
10.1006/jsco.1996.0030
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.sciencedirect.com
)
(
www.informatik.unitrier.de
)
(
linkinghub.elsevier.com
)
(
reference.kfupm.edu.sa
)
More »
Citation Context
(65)
...The set of assigned literals in any of the leaves of such a decomposition tree is then called a guiding path (
Zhang, Bonacina, and Hsiang 1996
)...
Youssef Hamadi
,
et al.
Seven Challenges in Parallel SAT Solving
...This early version of claspar used the wellknown guiding path technique [
4
] for splitting the search space into disjoint parts...
Martin Gebser
,
et al.
ClusterBased ASP Solving with
...A typical approach to splitting the search space is to use guiding path or semantic decomposition based techniques [8,9,
10
,11,12,13]...
...The plain partitioning approach bears close resemblance to the guiding path approach [
10
,17], and, provided that the derived instances always have lower run time than the original instance, the plain partitioning approach can solve arbitrarily difficult problems given a sufficiently large n [14]...
Antti Eero Johannes Hyvärinen
,
et al.
Partitioning SAT Instances for Distributed Solving
...PSATO [
21
] and Gradsat [2], [3] are two examples for high end parallel solvers, which consist of bringing their sequential counterparts ([20] and [15]) to a parallel platform...
Quirin Meyer
,
et al.
3SAT on CUDA: Towards a massively parallel SAT solver
...[2]). They generally divide the search space using the well known guidingpath concept [
3
]...
Long Guo
,
et al.
Diversification and Intensification in Parallel SAT Solving
References
(17)
Solving Open Quasigroup Problems by Propositional Reasoning
(
Citations: 18
)
Hantao Zhang
Published in 1994.
Automated reasoning and exhaustive search: Quasigroup existence problems
(
Citations: 71
)
M. Stickel
,
Masayuki Fujita
Journal:
Computers & Mathematics With Applications  COMPUT MATH APPL
, vol. 29, no. 2, pp. 115132, 1995
A DavisPutnam program and its application to finiteorder model search: Quasigroup existence problems
(
Citations: 64
)
William Mccune
Published in 1994.
Automatic Generation of Some Results in Finite Algebra
(
Citations: 79
)
Masayuki Fujita
,
John K. Slaney
,
Frank Bennett
Conference:
International Joint Conference on Artificial Intelligence  IJCAI
, pp. 5259, 1993
Symbolic logic and mechanical theorem proving
(
Citations: 960
)
ChinLiang Chang
,
Richard C. T. Lee
Published in 1973.
Sort by:
Citations
(97)
Seven Challenges in Parallel SAT Solving
(
Citations: 1
)
Youssef Hamadi
,
Christoph M. Wintersteiger
Published in 2012.
Search: from Algorithms to Systems
Youssef Hamadi
Published in 2012.
ClusterBased ASP Solving with
Martin Gebser
,
Roland Kaminski
,
Benjamin Kaufmann
,
Torsten Schaub
,
Bettina Schnor
Conference:
Logic Programming and Nonmonotonic Reasoning  LPNMR
, pp. 364369, 2011
An investigation in parallel execution of answer set programs on distributed memory platforms: Task sharing and dynamic scheduling
(
Citations: 1
)
Enrico Pontelli
,
Hung Viet Le
,
Tran Cao Son
Journal:
Computer Languages, Systems & Structures  CL
, vol. 36, no. 2, pp. 158202, 2010
Partitioning SAT Instances for Distributed Solving
Antti Eero Johannes Hyvärinen
,
Tommi A. Junttila
,
Ilkka Niemelä
Conference:
Logic Programming and Automated Reasoning/Russian Conference on Logic Programming  LPAR(RCLP)
, pp. 372386, 2010