SATO: A Solver for Propositional Satisfiability

The Davis-Putnam method is one of the major practical methods for the satisfiability (SAT) problem of propositional logic. In the last decade, we developed a very efficient implementation of the Davis-Putnam method called SATO. 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.

The code of SATO4.2
The code of SATO3.2

The README 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 Technical Report, The University of Iowa, 1994.
• Zhang, H., Hsiang, J.: Solving open quasigroup problems by propositional reasoning . 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 , in 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.
• Zhang, H.: 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.
• Zhang, H.: SATO: An Efficient Propositional Prover , Proc. of International Conference on Automated Deduction (CADE-97).
• Zhang, H.: A random jump strategy for combinatorial search , Proc. of International Symposium on AI and Math, Fort Lauderdale, Florida, 2002.
• Zhang, H.: 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), Valencia, Spain.
• Shen, H., H. Zhang: An empirical study of MAX-2-SAT phase transition , Workshop on Typical Case Complexity and Phase Transitions, LICS 2003, Ottawa, Canada.