One of the cornerstone Conflict-Driven Clause Learning SAT solver algorithms is the DPLL algorithm.
Early branching Heuristics (Bohm's Heuristic, Maximum Occurrences on Minimum sized clauses heuristic, and Jeroslow-Wang heuristic) can be regarded as greedy algorithms.