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.

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


Papers related to SATO