Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
| العنوان: | Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers |
|---|---|
| المؤلفون: | Dawn Michaelson, Dominik Schreiber, Marijn J. H. Heule, Benjamin Kiesl-Reiter, Michael W. Whalen |
| المصدر: | 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 |
| بيانات النشر: | Springer Nature Switzerland, 2023. |
| سنة النشر: | 2023 |
| مصطلحات موضوعية: | distributed computing, SAT solving, DATA processing & computer science, proofs, ddc:004 |
| الوصف: | 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. |
| وصف الملف: | application/pdf |
| ردمك: | 978-3-031-30822-2 978-3-031-30823-9 |
| تدمد: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-031-30823-9_18 |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::f9e4076eaebdc682eeec5ecb8d660d7f https://doi.org/10.1007/978-3-031-30823-9_18 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....f9e4076eaebdc682eeec5ecb8d660d7f |
| قاعدة البيانات: | OpenAIRE |
| ردمك: | 9783031308222 9783031308239 |
|---|---|
| تدمد: | 03029743 16113349 |
| DOI: | 10.1007/978-3-031-30823-9_18 |