M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962.
DOI : 10.1145/368273.368557

A. Del and V. , On 2-SAT and Renamable Horn, Proceedings of the Seventeenth National Conference on Artificial Intelligence, pp.279-284, 2000.

M. Sharir, A strong-connectivity algorithm and its applications in data flow analysis, Computers & Mathematics with Applications, vol.7, issue.1, pp.67-72, 1981.
DOI : 10.1016/0898-1221(81)90008-0

R. Tarjan, Depth first search and linear graph algorithms, SIAM Journal on Computing, 1972.
DOI : 10.1109/swat.1971.10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.327.8418