Geodesic
Algorithms using ROBDD as a~base for Boolean constraints
Prikladnaâ diskretnaâ matematika, no. 1 (2010), pp. 86-104.

Voir la notice de l'article provenant de la source Math-Net.Ru

In the paper, we study algorithmic properties of ROBDD considered in the role of Boolean constraints in the hybrid (SAT+ROBDD) logical derivation. We suggest ROBDD-analogs for the basic algorithmic procedures used in DPLL-derivation such as variable assignment, unit clause, clause learning, and the techniques of delayed computations. A new algorithm intended for ROBDD reordering is proposed. Computational complexity of all the considered algorithms is provided.
Keywords: logical equations, binary decision diagrams, hybrid logical derivation. 
@article{PDM_2010_1_a6,
     author = {A. S. Ignatiev and A. A. Semenov},
     title = {Algorithms using {ROBDD} as a~base for {Boolean} constraints},
     journal = {Prikladna\^a diskretna\^a matematika},
     pages = {86--104},
     publisher = {mathdoc},
     number = {1},
     year = {2010},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDM_2010_1_a6/}
}
TY  - JOUR
AU  - A. S. Ignatiev
AU  - A. A. Semenov
TI  - Algorithms using ROBDD as a~base for Boolean constraints
JO  - Prikladnaâ diskretnaâ matematika
PY  - 2010
SP  - 86
EP  - 104
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/PDM_2010_1_a6/
LA  - ru
ID  - PDM_2010_1_a6
ER  - 
%0 Journal Article
%A A. S. Ignatiev
%A A. A. Semenov
%T Algorithms using ROBDD as a~base for Boolean constraints
%J Prikladnaâ diskretnaâ matematika
%D 2010
%P 86-104
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/PDM_2010_1_a6/
%G ru
%F PDM_2010_1_a6
A. S. Ignatiev; A. A. Semenov. Algorithms using ROBDD as a~base for Boolean constraints. Prikladnaâ diskretnaâ matematika, no. 1 (2010), pp. 86-104. http://geodesic.mathdoc.fr/item/PDM_2010_1_a6/

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

[2] http://www.isa.ewi.tudelft.nl/jsat

[3] Hachtel G. D., Somenzi F., Logic synthesis and verification algorithms, Kluwer Ac. Publ., 2002

[4] Klark E. M., Gramberg O., Peled D., Verifikatsiya modelei programm: Model Checking, MTsNMO, M., 2002

[5] Garanina N. O., Shilov N. V., “Verifikatsiya kombinirovannykh logik znanii, deistvii i vremeni v modelyakh”, Sistemnaya informatika, 2005, no. 10, 114–173

[6] Semenov A. A., Zaikin O. S., Bespalov D. V., Ushakov A. A., “SAT-podkhod v kriptoanalize nekotorykh sistem potochnogo shifrovaniya”, Vychislitelnye tekhnologii, 13:6 (2008), 134–150

[7] Sistemnaya kompyuternaya biologiya, eds. N. A. Kolchanov, S. S. Goncharov, V. A. Likhoshvai, V. A. Ivanisenko, Izd-vo SO RAN, Novosibirsk, 2008, 767 pp.

[8] Davis M., Logemann G., Loveland D., “A machine program for theorem proving”, Comm. ACM, 5 (1962), 394–397 | DOI | MR | Zbl

[9] Marqeus-Silva J. P., Sakallah K. A., “GRASP: A search algorithm for propositional satisfiability”, IEEE Trans. Comp., 48:5 (1999), 506–521 | DOI | MR

[10] Moskewicz M., Madigan C., Zhao Y., et al., “Chaff: Engineering an Efficient SAT Solver”, Proc. Design Automat. Conf. (DAC), 2001, 530–535

[11] MiniSat, http://minisat.se/MiniSat.html

[12] Semenov A. A., Zaikin O. S., “Nepolnye algoritmy v krupnoblochnom parallelizme kombinatornykh zadach”, Vychislitelnye metody i programmirovanie, 9 (2008), 108–118

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

[14] Zakrevskii A. D., Logicheskie uravneniya, Nauka i tekhnika, Minsk, 1975 | MR | Zbl

[15] Semenov A. A., Bespalov D. V., “Tekhnologii resheniya mnogomernykh zadach logicheskogo poiska”, Vestnik Tomskogo gosuniversiteta, 2005, Prilozhenie No 14, 61–73

[16] Zhang L., Madigan C., Moskewicz M., Malik S., “Efficient conflict driven learning in a boolean satisfiability solver”, Proc. Intern. Conf. on Computer Aided Design (ICCAD), 2001, 279–285

[17] Lynce I., Marques-Silva J. P., “Efficient data structures for backtrack search SAT solvers”, Ann. Mathem. Artific. Intellig., 43 (2005), 137–152 | MR | Zbl

[18] Semenov A. A., Zaikin O. S., Bespalov D. V. i dr., “Reshenie zadach obrascheniya diskretnykh funktsii na mnogoprotsessornykh vychislitelnykh sistemakh”, Trudy Chetvertoi Mezhdunar. konf. PACO'2008 (Moskva, 26–29 oktyabrya 2008), M., 2008, 152–176

[19] Zaikin O. S., Semenov A. A., “Tekhnologiya krupnoblochnogo parallelizma v SAT-zadachakh”, Problemy upravleniya, 2008, no. 1, 43–50

[20] Semenov A. A., “Translyatsiya algoritmov vychisleniya diskretnykh funktsii v vyrazheniya propozitsionalnoi logiki”, Prikladnye algoritmy v diskretnom analize. Ser. Diskretnyi analiz i informatika, 2008, no. 2, 70–98

[21] Cook S. A., “The complexity of theorem-proving procedures”, Proc. 3rd Ann. ACM Symp. on Theory of Computing, ACM, 1971, 151–159; Kuk S. A., “Slozhnost protsedur vyvoda teorem”, Kiberneticheskii sbornik. Novaya seriya, 1975, no. 12, 5–15

[22] Lee C. Y., “Representation of Switching Circuits by Binary-Decision Programs”, Bell Systems Technical J., 38 (1959), 985–999 | MR

[23] Bryant R. E., “Graph-Based Algorithms for Boolean Function Manipulation”, IEEE Trans. Comp., 35:8 (1986), 677–691 | DOI | Zbl

[24] Meinel Ch., Theobald T., Algorithms and Data Structures in VLSI-Design: OBDD-Foundations and Applications, Springer-Verlag, 1998

[25] Khmelnov A. E., Ignatev A. S., Semenov A. A, “Dvoichnye diagrammy reshenii v logicheskikh uravneniyakh i zadachakh obrascheniya diskretnykh funktsii”, Vestnik NGU. Ser. Informatsionnye tekhnologii, 7:4 (2009), 36–52

[26] Semenov A. A., “O preobrazovaniyakh Tseitina v logicheskikh uravneniyakh”, Prikladnaya diskretnaya matematika, 2009, no. 4, 28–50

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

[28] Beame P., Kautz H., Sabharwal A., “Understanding the power of clause learning”, Proc. Of 18th Intern. Joint Conf. on Artificial Intellegence, IJCAI, 2003, 1194–1201

[29] Ignatev A. S., Semenov A. A., Khmelnov A. E., “Ispolzovanie dvoichnykh diagramm reshenii v zadachakh obrascheniya diskretnykh funktsii”, Vestnik Tomskogo gosuniversiteta. Ser. Upravlenie, vychislitelnaya tekhnika, informatika, 2009, no. 1(6), 115–129

[30] Bryant R. E., “Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams”, ACM Comp. Surv., 24:3 (1992), 293–318 | DOI

[31] Levitin A., Algoritmy. Vvedenie v razrabotku i analiz, Vilyams, M., 2006

[32] Voevodin V. V., Voevodin Vl. V., Parallelnye vychisleniya, BKhV-Peterburg, SPb., 2002

[33] Schubert T., Lewis M., Becker B., “PaMiraXT: Parallel SAT Solving with Threads and Message Passing”, J. Satisf., Bool. Mod. Comp., 6 (2009), 203–222 | Zbl