The Davis and Putnam (D&P) scheme has been intensively studied during this last decade. Nowadays, its good empirical perfor-
mances are well-known. Here, we deal with its theoretical side which has been relatively less studied until now. Thus, we
propose a strictely lin- ear D&P algorithm for the most well known tractable classes: Horn-SAT and 2-SAT. Specifically, the
strictely linearity of our proposed D&P algo- rithm improves significantly the previous existing complexities that were quadratic
for Horn-SAT and even exponential for 2-SAT. As a conse- quence, the D&P algorithm designed to deal with the general SAT problem
runs as fast (in terms of complexity) as the specialised algorithms designed to work exclusively with a specific tractable
SAT subclass.
Keywords Automated Reasoning - Computational Complexity - Search - Theorem Proving