Geodesic
About convergence of a hybrid SAT+ROBDD-derivation
Prikladnaya Diskretnaya Matematika. Supplement, no. 5 (2012), pp. 118-120 
A. A. Semenov; A. S. Ignatiev. About convergence of a hybrid SAT+ROBDD-derivation. Prikladnaya Diskretnaya Matematika. Supplement, no. 5 (2012), pp. 118-120. http://geodesic.mathdoc.fr/item/PDMA_2012_5_a63/
@article{PDMA_2012_5_a63,
     author = {A. A. Semenov and A. S. Ignatiev},
     title = {About convergence of a~hybrid {SAT+ROBDD-derivation}},
     journal = {Prikladnaya Diskretnaya Matematika. Supplement},
     pages = {118--120},
     year = {2012},
     number = {5},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDMA_2012_5_a63/}
}
TY  - JOUR
AU  - A. A. Semenov
AU  - A. S. Ignatiev
TI  - About convergence of a hybrid SAT+ROBDD-derivation
JO  - Prikladnaya Diskretnaya Matematika. Supplement
PY  - 2012
SP  - 118
EP  - 120
IS  - 5
UR  - http://geodesic.mathdoc.fr/item/PDMA_2012_5_a63/
LA  - ru
ID  - PDMA_2012_5_a63
ER  - 
%0 Journal Article
%A A. A. Semenov
%A A. S. Ignatiev
%T About convergence of a hybrid SAT+ROBDD-derivation
%J Prikladnaya Diskretnaya Matematika. Supplement
%D 2012
%P 118-120
%N 5
%U http://geodesic.mathdoc.fr/item/PDMA_2012_5_a63/
%G ru
%F PDMA_2012_5_a63

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

In the paper, the authors consider a new property of a hybrid SAT+ROBDD-derivation. This property consists in a convergence with respect to the number of paths to a terminal vertex “1” in a ROBDD which represents database of conflicts accumulated during the process of non-chronological DPLL.

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

[2] Otpuschennikov I. V., Semenov A. A., “Tekhnologiya translyatsii kombinatornykh problem v bulevy uravneniya”, Prikladnaya diskretnaya matematika, 2011, no. 1, 96–115

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

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

[5] Ignatiev A. S., Semenov A. A., “DPLL+ROBDD derivation applied to inversion of some cryptographic functions”, LNCS, 6695, 2011, 76–89 | MR | Zbl

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