Finite Model Generation
The Davis-Putnam method is one of the major practical methods for
the satisfiability (SAT) problem of propositional logic. In the last
three years, we developed a very efficient implementation of the
Davis-Putnam method called SATO. We used the trie data structure for
propositional clauses by presenting seven implementations of the
method. We found a new technique for implementing unit propagation
whose complexity is better than any existing unit propagation
algorithms. The efficiency of our programs allowed us to solve over
one hundred open quasigroup problems in design theory. We also
experimented SATO on networked workstations by using a master-slave
model for communication. A simple and effective workload balancing
method distributes the workload among workstations.
File of SATO
Papers related to SATO
Kim, S., Zhang, H.:
ModGen: Theorem proving by model generation
Proc. of National Conference of American Association on
Artificial Intelligence (AAAI-94), Seattle, WA.
MIT Press, pp. 162-167.
Zhang, H., Stickel, M.:
Implementing Davis-Putnam's method
It appeared as a
The University of Iowa, 1994.
Zhang, H., Hsiang, J.:
Solving open quasigroup problems by
. Proc. of International Computer Symposium}, Hsinchu, Taiwan, 1994.
Zhang, H., Bonacina, M.P.:
Cumulating search in a distributed
computing environment: A case study in parallel satisfiability
Proc. of the First International Symposium on Parallel Symbolic
Computation (PASCO-94), Linz, Austria, September 1994.
Zhang, H., Stickel, M.:
An efficient algorithm for unit-propagation
Proc. of the Fourth International Symposium on Artificial
Intelligence and Mathematics. Ft. Lauderdale, Florida, 1996.
Zhang, H., Bonacina, M.P., Hsiang, H.:
PSATO: a Distributed Propositional Prover and its
Application to Quasigroup Problems
Journal of Symbolic Computation (1996) 21, 543-560.
Specifying Latin squares in propositional logic , in R. Veroff
(ed.): Automated Reasoning and Its Applications, Essays in honor of
Larry Wos, Chapter 6, MIT Press, 1997.
SATO: An Efficient Propositional Prover
, Proc. of International Conference on Automated Deduction
A random jump strategy for combinatorial search
, Proc. of International Symposium on AI and Math, Fort Lauderdale,
Generating college conference basketball schedules
by a SAT Solver
, Proc. of International Symposium on Satisfiability (SAT 2002)
Cincinantti, Ohio, 2002.
Zhang, H., H. Shen, F. Manya:
Exact algorithms for MAX-SAT
, International Workshop on First-Order Theorem Proving (FTP 2003),
Shen, H., H. Zhang:
An empirical study of MAX-2-SAT phase transition
, Workshop on Typical Case Complexity and Phase Transitions, LICS 2003,