|
Article information
2016 , Volume 21, ¹ 3, p.5-17
Bychkov I.V., Oparin G.A., Bogdanova V.G., Gorsky S.A., Pashinin A.A.
A multiagent technology of automation for parallel solution of Boolean equations in a distributed computing environment
Many practically important combinatorial problems can be reduced to the problem of determining the satisfiability of Boolean formulas (SAT). In recent years, there is a tendency to widespread the use of parallel technology for solving such problems in a distributed computing environment. The purpose of our research is to development the technology and to build the tools that provide the automation of all steps for solving this class of problems. These steps include the construction of a Boolean model, the parallel approach to solution of the resulting system of Boolean equations. It also include processing of solutions and providing an access to high-performance computing (HPC) resources for subject specialists. The special technique was developed to automate the construction of the Boolean model. This technique provides different ways of constructing Boolean model, which include the synthesis of Boolean constraints in DIMACS format. The sat-solver oriented for using a hybrid MPI+OpenMP programming model for HPC systems with clusters of shared memory nodes was designed to solve non-trivial SAT problem. The multi-agent system (MAS) was created for the organization of a three-level parallelism and management of parallel computations using the HpcSoMas framework which was also developed by the authors. This MAC generates a packet of tasks for the problem, allocates resources for this package, manages the execution of the tasks, and informs the user about the status of the task. The author provides experimental tests for a number of SAT instances have been performed using the presented approach and these experiments indicate the usefulness and effectiveness of SAT approach for automation technology.
[full text]
Keywords: Boolean equations and constraints, combinatorial problems, Boolean satisfiability
Author(s):
Bychkov Igor Vyacheslavovich
Dr. , Academician RAS, Professor
Position: Director
Office: Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952) 45-30-61
E-mail: idstu@icc.ru
SPIN-code: 5816-7451Oparin Gennady Anatoljevich
Dr. , Professor
Position: Deputy Director on science
Office: Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952) 45-30-61
E-mail: prn51@icc.ru
SPIN-code: 4544-2804Bogdanova Vera Gennadevna
PhD. , Associate Professor
Position: Senior Research Scientist
Office: Matrosov Institute for System Dynamics and Control Theory of SB RAS
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952) 45-30-93
E-mail: bvg@icc.ru
SPIN-code: 9123-3563Gorsky Sergey Alexeevich
PhD.
Position: Research Scientist
Office: Matrosov Institute for System Dynamics and Control Theory of SB RAS
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952) 453017
E-mail: gorsky@icc.ru
SPIN-code: 7347-1818Pashinin Anton Alexeevich
Position: Junior Research Scientist
Office: Matrosov Institute for System Dynamics and Control Theory of SB RAS
Address: 664033, Russia, Irkutsk, Lermontova st., 134
Phone Office: (3952) 453017
E-mail: apcrol@gmail.com
SPIN-code: 9325-0914 References:
[1] Levchenkov, V.S. Bulevy uravneniya [Boolean equations]. Moscow: Dialog MGU; 1999: 72. (In Russ.)
[2] Bohmann, D., Postkhoff, Kh. Dvoichnye dinamicheskie sistemy [Binary dynamical systems]. Moscow: Energoatomizdat; 1986: 401. (In Russ.)
[3] Chrabakh, W., Wolski, R. GridSAT: A Chaff-based distributed SAT solver for the grid. Proceedings of the 2003 ACM/IEEE Conference on Supercomputing. Washington: IEEE Computer Society; 2003: 37.
[4] Chrabakh, W., Wolski, R. GrADSAT: A Parallel SAT Solver for the Grid. UCSB Computer Science Technical Report Number 2003-05. USA: University of California Santa Barbara; 2003: 9.
[5] Oparin, G.A., Feoktistov, A.G., Bogdanova, V.G., Novopashin, A.P. The solution of high dimensionality Boolean Equations in distributed computing environment. Proc. of Distributed Computing and Grid-technologies in Science and Education. Dubna: OIYaI; 2004: 164–169. (In Russ.)
[6] Oparin, G.A., Feoktistov, A.G., Bogdanova, V.G., Novopashin, A.P. The toolkit for boolean modelling and solving Boolean Equations in the internet. Proc. of Distributed Computing and Grid-technologies in Science and Education. Dubna: OIYaI; 2006: 369–378. (In Russ.)
[7] Gil, L., Flores, P., Silveira, L.M. PMSat: A parallel version of Minisat. Journal on Satisability, Boolean Modeling and Computation. 2008; (6):71–98.
[8] Ohmura, K., Ueda, K. c-sat: A parallel SAT solver for clusters. Theory and Applications of Satisability Testing-SAT, ser. LNCS. Berlin / Heidelberg: Springer; 2009: (5584):524–537.
[9] Schulz, S., Blochinger, W. Parallel SAT solving on peer-to-peer desktop grids. Journal of Grid Computing. 2010; 8(3):443–471.
[10] Balyo, T., Sanders, P., Sinz, C. HordeSat: A massively parallel portfolio SAT solver. Theory and Applications of Satisfiability Testing — SAT 2015: Lecture Notes in Computer Science. Proceedings of the 18th International Conference. September 24–27, 2015. USA: Austin, TexasX; 2015: (9340):156–172.
[11] Een, N., Sorensson, N. MiniSat solver. Available at: http://minisat.se/ (accessed 12.12.2015).
[12] Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Technical Report 10/1, August 2010, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria; 2010: 4.
[13] Hamadi, Y., Jabbour, S., Sais, L. ManySAT: A parallel SAT solver. Journal on Satisfiability, Boolean Modeling and Computation. 2009; (6):245–262.
[14] Oparin, G.A., Bogdanova, V.G. Rebus - Intellectual Solver for Combinatorial Problems in Boolean Constraints. Novosibirsk State University Journal of Information Technologies. 2008; 6(1):61–69. (In Russ.)
[15] Oparin, G.A., Bogdanova, V.G., Makeeva, N.G. Toolkit for the the parallel solving of systems Boolean equations. Modern Technologies. System Analysis. Modeling. 2009; (3):62–68. (In Russ.)
[16] Oparin, G.A., Bogdanova, V.G. Parallel computing toolkit for solving Boolean Equations on multi-core processors. Programmnye Produkty i Sistemy. 2012; (1):10–14. (In Russ.)
[17] Bogdanova, V.G., Bychkov, I.V., Korsukov, A.S., Oparin, G.A., Feoktistov, A.G. Multiagent approach to controlling distributed computing in a cluster grid system. Journal of Computer and Systems Sciences International. 2014; 53(5):713–722.
[18] Bychkov, I.V., Oparin, G.A., Feoktistov, A.G., Bogdanova, V.G., Pashinin, A.A. Service-oriented multiagent control of distributed computations. Automation and Remote Control. 2015; 76(11):2000–2010.
[19] Bychkov, I.V., Oparin, G.A., Feoktistov, A.G., Bogdanova, V.G., Pashinin,A.A. Multiagent methods and tools of management in a service-oriented distributed computing environment. Proceedings of the Institute for System Programming of the RAS. 2005; 26(5):65–82. (In Russ.)
[20] Bogdanova, V.G., Gorskiy, S.A. The technology of parallel solution of nonlinear systems of boolean equations on a computing cluster. Modern Technologies. System Analysis. Modeling. 2013; 1(37):54–60. (In Russ.)
[21] Bogdanova, V.G., Gorskiy, S.A., Pashinin, A.A. Service-oriented tools for solving of Boolean satisfiability problem. Fundamental Research. 2015; 2(6):1151–1156. (In Russ.)
[22] Gorshkov, S.P. Application of the theory of NP-complete problems for estimation of the complexity for solutions of systems of Boolean equations. Obozrenie Prikladnoy i Promyshlennoy Matematiki. 1995; 2(3):325–398. (In Russ.)
[23] Yshakov, D.M., Telerman, V.V. Sistemy programmirovaniya v ogranicheniyakh. Sistemnaya informatika: Sbornik nauchykh trudov. Vypusk 7. Problemy teorii i metodologii sozdaniya [Systems of Constraint programming. System Informatics: Ñoll. of Scientific Papers. Vol. 7: Problems of the Theory and Methodology for Development of Parallel and Distributed Systems]. Novosibirsk: Nauka; 2000: 275–310. (In Russ.)
[24] Bychkov, I.V., Oparin, G.A., Feoktistov, A.G., Bogdanova, V.G., Korsukov, A.S. The service-oriented approach to distributed computing on the basis of the toolkit DISCENT. Information Technologies and Computer Systems. 2014; (2):7-15. (In Russ.)
[25] JavaScript object notation format. Available at: http://www.json.org/ (accessed 12.12.2015).
[26] Irkutsk supercomputer center of the Siberian Branch of the Russian Academy of Sciences. Available at: http://hpc.icc.ru (accessed 12.12.2015). (In Russ.)
[27] Karlsruhe Institute of Technology. HordeSat: A massively parallel portfolio SAT solver. Available at: http://baldur.iti.kit.edu/hordesat (accessed 12.12.2015).
Bibliography link:
Bychkov I.V., Oparin G.A., Bogdanova V.G., Gorsky S.A., Pashinin A.A. A multiagent technology of automation for parallel solution of Boolean equations in a distributed computing environment // Computational technologies. 2016. V. 21. ¹ 3. P. 5-17
|
