Abstract
Satciety is a distributed parallel satisfiability (SAT) solver which focuses on tackling the domain-specific problems inherent to one of the most challenging environments for parallel computing—Peer-to-Peer Desktop Grids. Satciety efficiently addresses issues related to resource volatility and heterogeneity, limited node and network capabilities, as well as non-uniform communication costs. This is achieved through a sophisticated distributed task pool execution model, problem size reduction through multi-stage SAT formula preprocessing, context-aware memory management, and adaptive topology-aware distributed dynamic learning. Despite the demanding conditions prevailing in Desktop Grids, Satciety achieves considerable speedups compared to state-of-the-art sequential SAT solvers.
Similar content being viewed by others
References
Anderson, D.P., Fedak, G.: The computational and storage potential of volunteer computing. In: Proc. of the Sixth IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2006), pp. 73–80. Singapore (2006)
Kondo, D., Taufer, M., Brooks, C.L., Casanova, H., Chien, A.A.: Characterizing and evaluating desktop Grids: an empirical study. In: Proc. of International Parallel and Distributed Processing Symposium. Sante Fe, New Mexico (2004)
Chien, A., Calder, B., Elbert, S., Bhatia, K.: Entropia: architecture and performance of an enterprise desktop Grid system. J. Parallel Distrib. Comput. 63, 597–610 (2003)
Anderson, D.P.: BOINC: a system for public-resource computing and storage. In: 5th IEEE/ACM International Workshop on Grid Computing, pp. 4–10. Pittsburgh, USA (2004)
Bhagwan, R., Savage, S., Voelker, G.: Understanding availability. In: Proceedings of the 2nd International Workshop on Peer-to-Peer Systems (IPTPS ’03), pp. 256–267 (2003)
Wolski, R., Spring, N., Hayes, J.: Predicting the cpu availability of time-shared unix systems on the computational Grid. In: Proc. of the the Eighth IEEE International Symposium on High Performance Distributed Computing, pp. 105–112. Washington, DC, USA (1999)
Verbeke, J., Nadgir, N., Ruetsch, G., Sharapov, I.: Framework for peer-to-peer distributed computing in a heterogeneous, decentralized environment. In: Proceedings of the Third International Workshop on Grid Computing (GRID ’02), London, UK, pp. 1–12. Springer (2002)
Tanaka, Y., Shudo, K., Sekiguchi, S.: P3: P2P-based middleware enabling transfer and aggregation of computational resources. In: Proc. Cluster Computing and Grid 2005 (Fifth Int’l Workshop on Global and Peer-to-Peer Computing). Cardiff, UK (2005)
Schulz, S., Blochinger, W., Held, M., Dangelmayr, C.: COHESION—A microkernel based desktop Grid platform for irregular task-parallel applications. Future Gener. Comput. Syst. (The International Journal of Grid Computing: Theory, Methods and Applications) 24(5), 354–370 (2008)
Cook, S.A.: The complexity of theorem proving procedures. In: 3rd Symp. on Theory of Computing, pp. 151–158. ACM Press (1971)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Tools and Algorithms for the Analysis and Construction of Systems (TACAS’99). LNCS, vol. 1579. Springer (1999)
Velev, M.N., Bryant, R.E.: Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. In: Proc. of the 38th Conference on Design Automation Conference (2001)
Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.: Combinational test pattern generation using satisfiability. IEEE Trans. Computer-Aided Design 15(9), 1167–1176 (1996)
Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proc. of the Tenth European Conference on Artificial Intelligence (ECAI’92), pp. 359–363 (1992)
Crawford, J.M., Baker, A.B.: Experimental results on the application of satisfiability algorithms to scheduling problems. In: Proc. of the Twelfth National Conference on Artificial Intelligence (AAAI-94), Seattle, Washington, vol. 2, pp. 1092–1097. AAAI Press/MIT Press (1994)
Massacci, F., Marraro, L.: Logical cryptanalysis as a SAT problem. J. Autom. Reason. 24(1–2), 165–203 (2000)
Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7(3), 201–215 (1960)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)
Marques-Silva, J.P., Sakallah, K.A.: Grasp—a new search algorithm for satisfiability. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design, pp. 220–227 (1996)
Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Proc. of 8th International Conference on Computer Aided Deduction (CADE 2002). Copenhagen, Denmark (2002)
Mitchell, D.G.: A SAT solver primer. EATCS Bulletin 85, 112–133 (2005)
Hooker, J.N., Vinay, V.: Branching rules for satisfiability. J. Autom. Reason. 15(3), 359–383 (1995)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference, pp. 530–535. Las Vegas (2001)
Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proc. of ICCAD. San Jose, CA (2001)
Grama, A., Gupta, A., Karypis, G., Kumar, V.: Introduction to Parallel Computing, 2nd edn. Addison-Wesley (2003)
Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a distributed propositional prover and its application to quasigroup problems. J. Symb. Comput. 21, 543–560 (1996)
Blochinger, W., Westje, W., Küchlin, W., Wedeniwski, S.: ZetaSAT—Boolean satisfiability solving on desktop Grids. In: Proc. of the Fifth IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2005), vol. 2, pp. 1079–1086. Cardiff, UK (2005)
Chrabakh, W., Wolski, R.: GridSAT: a Chaff-based distributed SAT solver for the Grid. In: Proc. of Supercomputing 03. Phoenix, Arizona, USA (2003)
Jurkowiak, B., Li, C.M., Utard, G.: A parallelization scheme based on work stealing for a class of SAT solvers. J. Autom. Reason. 34(1), 73–101 (2005)
Blochinger, W., Dangelmayr, C., Schulz, S.: Aspect-oriented parallel discrete optimization on the Cohesion desktop Grid platform. In: Proc. of the Sixth IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2006), pp. 49–56. Singapore (2006)
Schulz, S., Blochinger, W., Hannak, H.: Capability-aware information aggregation in peer-to-peer Grids—methods, architecture, and implementation. Journal of Grid Computing 7(2), 135–167 (2009)
Ganesh, A.J., Kermarrec, A.-M., Massoulié, L.: Peer-to-Peer membership management for gossip-based protocols. IEEE Trans. Comput. 52(2), 139–149 (2003)
Schulz, S., Blochinger, W., Poths, M.: Orbweb—a network substrate for peer-to-peer Grid computing based on open standards. Journal of Grid Computing 8(1), 77–107 (2010)
The XMPP Software Foundation: http://www.xmpp.org. Last accessed: March 2010
Blumofe, R.D., Leiserson, C.E.: Scheduling multithreaded computations by work stealing. J. ACM 46(5), 720–748 (1999)
Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)
Matocha, J., Camp, T.: A taxonomy of distributed termination detection algorithms. J. Syst. Softw. 43(3), 207–221 (1998)
DeMara, R.F., Tseng, Y., Ejnioui, A.: Tiered algorithm for distributed process quiescence and termination detection. IEEE Trans. Parallel Distrib. Syst. 18(11), 1529–1538 (2007)
Dhamdhere, D.M., Iyer, S.R., Reddy, E.K.K.: Distributed termination detection for dynamic systems. Parallel Comput. 22(14), 2025–2045 (1997)
Stupp, G.: Stateless termination detection. In: DISC ’02: Proceedings of the 16th International Conference on Distributed Computing, London, UK, pp. 163–172. Springer (2002)
Mittal, N., Venkatesan, S., Peri, S.: Message-optimal and latency-optimal termination detection algorithms for arbitrary topologies. In: Proc. 18th Ann. Conf. Distributed Computing (DISC ’04) (2004)
Xu, C., Lau, F.C.M.: Efficient termination detection for loosely synchronous applications in multicomputers. IEEE Trans. Parallel Distrib. Syst. 7(5), 537–544 (1996)
Cohen, S., Lehmann, D.: Dynamic systems and their distributed termination. In: PODC ’82: Proceedings of the First ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, New York, NY, USA, pp. 29–33. ACM (1982)
Dijkstra, E.W., Scholten, C.S.: Termination detection for diffusing computations. Inf. Process. Lett. 11(1), 1–4 (1980)
Misra, J., Chandy, K.M.: Termination detection of diffusing computations in communicating sequential processes. ACM Trans. Program. Lang. Syst. 4(1), 37–43 (1982)
Lai, T.-H.: Termination detection for dynamically distributed systems with non-first-in-first-out communication. J. Parallel Distrib. Comput. 3(4), 577–599 (1986)
Mattern, F.: Global quiescence detection based on credit distribution and recovery. Inf. Process. Lett. 30(4), 195–200 (1989)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) Theory and Applications of Satisfiability Testing: 6th International Conference, SAT 2003. LNCS, vol. 2919, pp. 502—518. Santa Margherita Ligure, Italy. Springer (2003)
Chrabakh, W., Wolski, R.: Gridsat: a system for solving satisfiability problems using a computational Grid. Parallel Comput. 32(9), 660–687 (2006)
Hyvärinen, A.E.J., Junttila, T., Niemelä, I.: Incorporating learning in Grid-based randomized SAT solving. In: Proceedings of the 13th International Conference on Artificial Intelligence: Methodology, Systems, and Applications, pp. 247–261. Varna, Bulgaria (2008)
Satisfiability—suggested format, May 1993. http://www.satlib.org/Benchmarks/SAT/satformat.ps. Last accessed: March 2010
The SAT Competition 2007 website. http://www.satcompetition.org/2007/. Last accessed: March 2010
The SAT Race 2008 website. http://www-sr.informatik.uni-tuebingen.de/sat-race-2008/. Last accessed: March 2010
Anbulagan, Slaney, J.: Multiple preprocessing for systematic SAT solvers. In: Proceedings of the 6th International Workshop on the Implementation of Logics. Phnom Penh, Cambodia (2006)
Eén, N., Biere, A.: Effective preprocessing in sat through variable and clause elimination. In: Proc. 8th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT’05). Lecture Notes in Computer Science (LNCS), vol. 3569. Springer (2005)
Bittorrent: http://www.bittorrent.com/protocol.html. Last accessed: March 2010
Liao, W.-C., Papadopoulos, F., Psounis, K.: Performance analysis of BitTorrent-like systems with heterogeneous users. Perform. Eval. 64(9–12), 876–891 (2007)
Spring, N., Peterson, L., Bavier, A., Pai, V.: Using planetlab for network research: myths, realities, and best practices. ACM SIGOPS Oper. Syst. Rev. 40(1), 17–24 (2006)
Wolski, R., Nurmi, D., Brevik, J.: An analysis of availability distributions in Condor. In: Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, pp. 1–6 (2007)
Blochinger, W.: Towards robustness in parallel SAT solving. In: Parallel Computing: Current & Future Issues of High-End Computing (Proc. of the International Conference ParCo 2005). Malaga, Spain (2006)
Rasterbar Software website. http://www.rasterbar.com/. Last accessed: March 2010
SAT Competition. http://www.satcompetition.org . Last accessed: March 2010
Biere, A.: Adaptive restart strategies for conflict driven SAT solvers. In: Büning, H.K., Zhao, X. (eds.) SAT. Lecture Notes in Computer Science, vol. 4996, pp. 28–33. Springer (2008)
Feldman, Y., Dershowitz, N., Hanna, Z.: Parallel multithreaded satisfiability solver: design and implementation. In: 3rd International Workshop on Parallel and Distributed Methods in Verification (PDMC 2004). London, UK (2004)
Singer, D., Vagner, A.: Parallel resolution of the satisfiability problem (SAT) with openmp and mpi. In: 6th International Conference on Parallel Processing and Applied Mathematics, PPAM 2005, pp. 380–388 (2005)
Lewis, M., Schubert, T., Becker, B.: Multithreaded SAT solving. In: 12th Asia and South Pacific Design Automation Conference, pp. 926–931 (2007)
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation 6, 245–262 (2009)
Boehm, M., Speckenmeyer, E.: A fast parallel SAT-solver—efficient workload balancing. Ann. Math. Artif. Intell. 17(3–4), 381–400 (1996)
Schubert, T., Lewis, M., Becker, B.: PaMiraXT: parallel SAT solving with threads and message passing. Journal on Satisfiability, Boolean Modeling and Computation 6, 203–222 (2009)
Blochinger, W., Sinz, C., Küchlin, W.: Parallel propositional satisfiability checking with distributed dynamic learning. Parallel Comput. 29(7), 969–994 (2003)
Chrabakh, W., Wolski, R.: Gridsat: design and implementation of a computational Grid application. Journal of Grid Computing 5(2), 177–193 (2006)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Schulz, S., Blochinger, W. Parallel SAT Solving on Peer-to-Peer Desktop Grids. J Grid Computing 8, 443–471 (2010). https://doi.org/10.1007/s10723-010-9160-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10723-010-9160-1