Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
| Autor: | Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Zdroj: | Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783031308222 Lecture Notes in Computer Science Lecture Notes in Computer Science-Tools and Algorithms for the Construction and Analysis of Systems |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-031-30823-9_18 |
| Popis: | Distributed clause-sharing SAT solvers can solve problems up to one hundred times faster than sequential SAT solvers by sharing derived information among multiple sequential solvers working on the same problem. Unlike sequential solvers, however, distributed solvers have not been able to produce proofs of unsatisfiability in a scalable manner, which has limited their use in critical applications. In this paper, we present a method to produce unsatisfiability proofs for distributed SAT solvers by combining the partial proofs produced by each sequential solver into a single, linear proof. Our approach is more scalable and general than previous explorations for parallel clause-sharing solvers, allowing use on distributed solvers without shared memory. We propose a simple sequential algorithm as well as a fully distributed algorithm for proof composition. Our empirical evaluation shows that for large-scale distributed solvers (100 nodes of 16 cores each), our distributed approach allows reliable proof composition and checking with reasonable overhead. We analyze the overhead and discuss how and where future efforts may further improve performance. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|