Using BOINC desktop grid to solve large scale SAT problems

• Autorzy: Posypkin M. , Semenov A. , Zaikin O.
• Języki publikacji: EN

Abstrakty

EN

Many practically important combinatorial problems can be efficiently reduced to a problem of Boolean satisfiability (SAT). Therefore, the implementation of distributed algorithms for solving SAT problems is of great importance. In this article we describe a technology for organizing desktop grid, which is meant for solving SAT problems. This technology was implemented in the form of a volunteer computing project SAT@home based on a popular BOINC platform.

Słowa kluczowe

EN

desktop grid; Boolean satisfiability problem (SAT); SAT; volunteer computing; BOINC

• Wydawca: Wydawnictwa AGH
• Czasopismo: Computer Science
• Rocznik: 2012
• Tom: Vol. 13 (1)
• Strony: 25--34
• Opis fizyczny: Bibliogr. 29 poz., rys., wykr.

Twórcy

autor

Posypkin M.

• Institute for Systems Analysis of RAS, Moscow, Russia

autor

Semenov A.

• Institute for System Dynamics and Control Theory of SB RAS, Irkutsk, Russia

autor

Zaikin O.

• Institute for System Dynamics and Control Theory of SB RAS, Irkutsk, Russia

Bibliografia

• [1] Eds. Biere A., Heule M., van Maaren H., Walsh T.: Handbook of Satisfiability. IOS Press, 2009.
• [2] Up-to-date links for the SATisfiability Problem. http://www.satlive.org/
• [3] Zaikin O., Semenov A.: Large-block parallelism technology in SAT problems. Control Sciences, No. 1, 2008, pp. 43–50 (in Russian).
• [4] Semenov A., Zaikin O., Bespalov D., Posypkin M.: Parallel logical cryptanalysis of the generator A5/1 in BNB-Grid system. Lecture Notes in Computer Science, vol. 6873, 2011, pp. 473–483.
• [5] Semenov A., Zaikin O., Bespalov D., Posypkin M.: Parallel algorithms for SAT in application to inversion problems of some discrete functions. arXiv:1102.3563v1 [cs.DC].
• [6] Schulz S., Blochinger W.: Parallel SAT Solving on Peer-to-Peer Desktop Grids. Journal Of Grid Computing, vol. 8, No. 3, 2010, pp. 443–471.
• [7] Anderson D.P.: Boinc: A system for public-resource computing and storage. [in:] Fifth IEEE/ACM International Workshop on Grid Computing, 2004, pp. 4–10.
• [8] Desktop Grids for eScience, – A Road map. Produced by DEGISCO. http://desktopgridfederation.org/documents/10508/57919/RoadMapD.pdf
• [9] Cappello F., Djilali S., Fedak G., Herault T., Magniette F., Neri V., LodygenskyO.: Computing on Large Scale Distributed Systems: XtremWeb Architecture, Programming Models,Security, Tests and Convergence with Grid Future Generation Computer Science, 2005, pp. 417–437.
• [10] Cirne W., Brasileiro F., Andrade N, Costa L.B., Andrade A., Novaes R., Mowbray M.: Labs of the World, Unite!!! Journal of Grid Computing, vol. 4, issue 3, 2006, pp. 225–246.
• [11] Litzkow M., Livny M., Mutka M.: Condor — A Hunter of Idle Workstations. [in:] Proc. The 8th International Conference of Distributed Computing Systems, San Jose, California, June, 1988, pp. 204–111.
• [12] Davis M., Logemann G., Loveland D.: A machine program for theorem proving. Communication of the ACM, vol. 5, 1962, pp. 394–397.
• [13] Marqeus-Silva J.P., Sakallah K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, vol. 48, No. 5, 1999, pp. 506–521.
• [14] Bohm M., Speckenmeyer E.: A fast parallel SAT solver — efficient workload balancing. Annals of Mathematics and Artificial Intelligence, vol. 17, No. 2, 1996, pp. 381–400.
• [15] Hamadi Y., Jabbour S., Sais L.: ManySAT: a Parallel SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving, vol. 6, 2009, pp. 245–262.
• [16] Schubert T., Lewis M., Becker B.: PaMiraXT: Parallel SAT Solving with Threads and Message Passing. Journal on Satisfiability, Boolean Modeling and Computation, vol. 6, 2009, pp. 203–222.
• [17] Soos M., Nohl K., Castelluccia C.: Extending SAT Solvers to Cryptographic Problems. Lecture Notes in Computer Science, vol. 5584, 2009, pp. 244–257.
• [18] Menezes A., Van Oorschot P., Vanstone S.: Handbook of Applied Cryptography. USA, CRC Press, 1996.
• [19] Quadratic Assignment Problem Library http://www.seas.upenn.edu/qaplib/
• [20] Colbourn C. J., Dinitz J.H.: Handbook of Combinatorial Designs. Chapman & Hall / Taylor & Francis, 2007.
• [21] Eds. Bower J. M., Bolouri H.: Computational Modeling of Genetic and Biochemical Networks, MITPress, 2004.
• [22] Volunteer computing project SAT@home http://sat.isa.ru/pdsat/
• [23] Kacsuk P., Kovacs J., Farkas Z., Marosi A. C., Gombas G., Balaton Z.: SZTAKI Desktop Grid (SZDG): A Flexible and Scalable Desktop Grid System. Journal of Grid Computing, vol. 7, No. 4, 2009, pp. 439–461.
• [24] Balaton Z., Gombas G., Kacsuk P., Kornafeld A., Kovacs J., Marosi A.C., Vida G., Podhorszki N., Kiss T.: Sztaki desktop grid: a modular and scalable way of building large computing grids. [in:] Proc. of the 21th Int. Parallel and Distributed Processing Symposium, Long Beach, California, USA, 2007, pp. 1–8.
• [25] The MiniSat page http://minisat.se/MiniSat.html
• [26] Supercomputer center of ISDCT SB RAS http://www.mvs.icc.ru/
• [27] Distributed computing stats system Free-DC http://stats.free-dc.org/
• [28] A5/1 Cracking project http://reflextor.com/trac/a51/wiki
• [29] Solutions found in SAT@home http://sat.isa.ru/pdsat/solutions.php