
There are 3 algorithms described on Wikipedia.
When I was undergrad, I came up with a solution using strongly connected components. The crucial observation is that (x or y) is equivalent to (not x > y) and (not y > x). Now you have a graph containing x, (not x) for all variables x and implications can be viewed as oriented edges  this is called implication graph.
Implication is transitive, so x > y and y > z implies x > z. This is the same as doing two steps in the implication graph.
If you have both (x > not x) and (not x > x), you have a contradiction. So you need to check if x and (not x) lie in the same strongly connected component in the implication graph. This can be done in linear time.
Finding a satisfying assignment is a bit more tricky, but can be done once you have the strongly connected components. 