Geodesic
Algorithms for constructing decomposition sets in application to coarse-grained parallelization of SAT problems
The Bulletin of Irkutsk State University. Series Mathematics, Tome 5 (2012) no. 4, pp. 79-94
Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

In the paper algorithms for constructing decomposition sets in application to coarse-grained parallelization of SAT problems are suggested. These sets are used for solving SAT problems in distributed computing environments. Suggested algorithms are based on computing scheme of Monte-Carlo method.
Keywords: Monte-Carlo method; discrete functions; SAT problems; coarse-grained parallelization. 
@article{IIGUM_2012_5_4_a7,
     author = {A. A. Semenov and O. S. Zaikin},
     title = {Algorithms for constructing decomposition sets in application to coarse-grained parallelization of {SAT} problems},
     journal = {The Bulletin of Irkutsk State University. Series Mathematics},
     pages = {79--94},
     year = {2012},
     volume = {5},
     number = {4},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/IIGUM_2012_5_4_a7/}
}
TY  - JOUR
AU  - A. A. Semenov
AU  - O. S. Zaikin
TI  - Algorithms for constructing decomposition sets in application to coarse-grained parallelization of SAT problems
JO  - The Bulletin of Irkutsk State University. Series Mathematics
PY  - 2012
SP  - 79
EP  - 94
VL  - 5
IS  - 4
UR  - http://geodesic.mathdoc.fr/item/IIGUM_2012_5_4_a7/
LA  - ru
ID  - IIGUM_2012_5_4_a7
ER  - 
%0 Journal Article
%A A. A. Semenov
%A O. S. Zaikin
%T Algorithms for constructing decomposition sets in application to coarse-grained parallelization of SAT problems
%J The Bulletin of Irkutsk State University. Series Mathematics
%D 2012
%P 79-94
%V 5
%N 4
%U http://geodesic.mathdoc.fr/item/IIGUM_2012_5_4_a7/
%G ru
%F IIGUM_2012_5_4_a7
A. A. Semenov; O. S. Zaikin. Algorithms for constructing decomposition sets in application to coarse-grained parallelization of SAT problems. The Bulletin of Irkutsk State University. Series Mathematics, Tome 5 (2012) no. 4, pp. 79-94. http://geodesic.mathdoc.fr/item/IIGUM_2012_5_4_a7/

[1] A. Biere, V. Heule, H. van Maaren, T. Walsh, Handbook of Satisfiability, IOS Press, 2009, 980 pp. | Zbl

[2] http://www.satlive.org

[3] T. Schubert, M. Lewis, B. Becker, “PaMiraXT: Parallel SAT Solving with Threads and Message Passing”, Journal on Satisfiability, Boolean Modeling and Computation, 6 (2009), 203–222 | Zbl

[4] Y. Hamadi, S. Jabbour, L. Sais, “ManySAT: a Parallel SAT Solver”, Journal on Satisfiability, Boolean Modeling and Computation, 6 (2009), 245–262 | Zbl

[5] A. Ignatiev, A. Semenov, “DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions”, LNCS, 6695, 2011, 76–89 | MR | Zbl

[6] S. Schulz, W. Blochinger, “Parallel SAT Solving on Peer-to-Peer Desktop Grids”, Journal Of Grid Computing, 8:3 (2010), 443–471 | DOI

[7] A. Hyvarinen, I. Niemela, T. Junttila, “Grid-Based SAT Solving with Iterative Partitioning and Clause Learning”, LNCS, 6876, 2011, 385–399

[8] M. Posypkin, A. Semenov, O. Zaikin, “Using BOINC desktop grid to solve large scale SAT problems”, Computer Science Journal, 13:1 (2012), 25–34 | DOI

[9] M. Davis, G. Logemann, D. Loveland, “A machine program for theorem proving”, Communication of the ACM, 5:7 (1962), 394–397 | DOI | MR | Zbl

[10] J. P. Marques-Silva, K. A. Sakallah, “GRASP: A search algorithm for propositional satisfiability”, IEEE Transactions on Computers, 48:5 (1999), 506–521 | DOI | MR

[11] N. Metropolis, S. Ulam, “The Monte Carlo method”, J. Amer. statistical assoc., 44:247 (1946), 335–341 | DOI | MR

[12] S. V. Ermakov, Metod Monte-Karlo i smezhnye voprosy, Nauka, M., 1971, 327 pp. | MR | Zbl

[13] A. S. Strekalovskii, Elementy nevypukloi optimizatsii, Nauka, Novosibirsk, 2003, 355 pp.

[14] G. S. Tseitin, “O slozhnosti vyvoda v ischislenii vyskazyvanii”, Zapiski nauchnykh seminarov LOMI AN SSSR, 8, 1968, 234–259

[15] M. Jarvisalo, T. Junttila, “Limitations of restricted branching in clause learning”, Constraints, 14:3 (2009), 325–356 | DOI | MR | Zbl

[16] A. A. Semenov, “Dekompozitsionnye predstavleniya logicheskikh uravnenii v zadachakh obrascheniya diskretnykh funktsii”, Izv. RAN. Teoriya i sistemy upravleniya, 2009, no. 5, 47–61

[17] W. Dowling, J. Gallier, “Linear-time algorithms for testing the satisfiability of propositional Horn formulae”, Journal of Logic Programming, 1:3 (1984), 267–284 | DOI | MR | Zbl

[18] Kh. Papadimitriu, K. Staiglits, Kombinatornaya optimizatsiya, Mir, M., 1985, 510 pp. | MR

[19] F. Glover, M. Laguna, Tabu Search, Kluwer Acad. Publ., Dordrecht, 1997 | MR

[20] S. Kirkpatrick, C. D. Gelatt, M. P. Vecchi, “Optimization by simulated annealing”, Science, 220 (1983), 671–680 | DOI | MR | Zbl

[21] http://hpc.icc.ru/hardware/blackford.php

[22] A. Biryukov, A. Shamir, D. Wagner, “Real time cryptanalysis of A5/1 on a PC”, LNCS, 1978, 2001, 1–18 | Zbl

[23] A. Semenov, O. Zaikin, D. Bespalov, M. Posypkin, “Parallel logical cryptanalysis of the generator A5/1 in BNB-Grid system”, LNCS, 6873, 2011, 473–483