PaSAT – parallel SAT-checking with lemma exchange: Implementation and applications. (English) Zbl 0990.90563
Kautz, Henry (ed.) et al., LICS 2001 workshop on theory and application of satisfiability testing (SAT 2001). Boston, MA, USA, June 14-15, 2001. Amsterdam: Elsevier, Electron. Notes Discrete Math. 9, no pag., electronic only (2001).
Summary: We present PaSAT, a parallel implementation of a Davis-Putnam-style propositional satisfiability checker incorporating dynamic search space partitioning, intelligent backjumping, as well as lemma generation and exchange; the main focus of our implementation is on speeding up SAT-checking of propositional encodings of real-world combinatorial problems. We investigate and analyze the speed-ups obtained by parallelization in conjunction with lemma exchange and describe the effects we observed during our experiments. Finally, we present performance measurements from the application of our prover in the areas of formal consistency checking of industrial product documentation, cryptanalysis, and hardware verification.
For the entire collection see [Zbl 0968.90001].
For the entire collection see [Zbl 0968.90001].
MSC:
| 90C27 | Combinatorial optimization |
Keywords:
Davis-Putnam-styleReferences:
| [1] | Biere, A.; Cimatti, A.; Clarke, E.; Zhu, Y.: Symbolic model checking without bdds. (1999) · Zbl 1046.68578 |
| [2] | Blochinger, Wolfgang; Küchlin, Wolfgang; Ludwig, Christoph; Weber, Andreas: An object-oriented platform for distributed high-performance symbolic computation. Mathematics and computers in simulation 49, 161-178 (1999) |
| [3] | Bryant, R. E.: Graph-based algorithms for Boolean function manipulation. IEEE transactions on computers 35, No. 8, 677-691 (Aug. 1986) · Zbl 0593.94022 |
| [4] | Böhm, M.; Speckenmeyer, E.: A fast parallel SAT-solver – efficient workload balancing. Annals of mathematics and artificial intelligence 17, No. 3-4, 381-400 (1996) · Zbl 0891.68096 |
| [5] | Blochinger, W.; Sinz, C.; Küchlin, W.: Parallel consistency checking of automotive product data. (2001) |
| [6] | Hooker, J. N.; Vinay, V.: Branching rules for satisfiability. Journal of automated reasoning 15, No. 3, 359-383 (1995) · Zbl 0838.68098 |
| [7] | Küchlin, W.; Sinz, C.: Proving consistency assertions for automotive product data management. Journal of automated reasoning 24, No. 1-2, 145-163 (February 2000) · Zbl 0968.68042 |
| [8] | Massacci, F.; Marraro, L.: Logical cryptanalysis as a sat problem. Journal of automated reasoning 24, No. 1-2, 165-203 (February 2000) · Zbl 0968.68052 |
| [9] | Silva, J. P. M.; Sakallah, K. A.: Conflict analysis in search algorithms for propositional satisfiability. Proceedings of the IEEE international conference on tools with artificial intelligence (Nov. 1996) |
| [10] | Zhang, H.; Bonacina, M. P.; Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. Journal of symbolic computation 21, 543-560 (1996) · Zbl 0863.68013 |
| [11] | Zhang, H.: Lemma generation in the Davis-Putnam method. Proceedings of the CADE-17 workshop on model computation (June 2000) |
| [12] | Zhang, H.; Stickel, M.: An efficient algorithm for unit propagation. (1996) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
