A tentative satisfiability algorithm
Problem 1

The case of $(x\rightarrow y \vee \overline y)$ should be a "non conditional variable" with respect to $x$ (ie. that $\overline x$ should now be inserted into $W$). If this is not true, then your algorithm needs an extra step to infer this. Assuming $(x\rightarrow y \vee \overline y)$ is a "non conditional variable", we continue.

Problem 2

NOTE: this is one problem I noticed; there may very well be other problems.

The problem is with the "empty OR implication" split into two algorithms, is that in its current form, the split does not cover all cases. In particular:

You start with $(x \vee c \rightarrow y)$, then $c$ is removed and we are left with an empty OR implication of $(x \vee [] \rightarrow y)$. You suggest now splitting it into two new problems and solving each of them; one with $x=T\wedge y=T$ and one where $y=T$. But this does not cover all cases. What about the case when $x=F\vee y=F$. However, your algorithm never considers the possibility that $y$ is false.

I think you might be able to fix this by formulating the two new problems as one with $y$ and one with $\overline x$.

Problem 3

What happens when you are left with a bunch of clauses in the form:

$$(a\wedge b \rightarrow c)$$

or

$$(a \rightarrow b \vee c)$$

After reducing everything, these clauses will remain, and you won't be able to test their satisfiability easily.

Analysis

Note: This "O" notation, $\mathcal{O}(something)$ etc., is called Big O notation. $\Omega(something)$ is called Big-omega.

Supposing the algorithm did work in general, it would run in time of $\Omega(2^m)$ worst case, $m$ being the number of variables. The reason is, each splitting of problem into problems of similar size means that the algorithm runs in exponential time. To visualize this concept, look at the following image of a full binary tree (image from here):



Now imagine the original problem is the node on top. We split the problem into two problems on the second level, but they are of similar size (we only get rid of one variable, $x$ or $y$ from the empty OR implication, so we will still have lots of empty OR implications to do each level). We will potentially have to split the problem $\mathcal{O}(m)$ times to get rid of $m$ variables. This means we will have to deal with a tree with $m$ levels. A tree with $m$ levels has $2^m$ leaf nodes (nodes at the bottom). This is called exponential time, and is informally somewhat on-par with all known boolean satisfiability algorithms. But so is brute force: there are $2^m$ possible assignments of the variables, so by brute force you can guess each assignment and check for satisfiability with similar performance!