A. A. Semenov, A. S. Ignatiev, “About convergence of a hybrid SAT+ROBDD-derivation”, Prikl. Diskr. Mat. Suppl., 2012, Issue 5,Pages <nobr>118

Computational methods in discrete mathematics

About convergence of a hybrid SAT+ROBDD-derivation

A. A. Semenov^a, A. S. Ignatiev^b

^a Institute of System Dynamics and Control Theory, Siberian Branch of the Russian Academy of Sciences, Irkutsk
^b Instituto de Engenharia de Sistemas e Computadores, Lisboa, Portugal

Abstract: 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.

UDC: 519.7