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