Possible Duplicate:
Best Upper Bounds on SAT
I'm working on the obstruction-set-free grid coloring problem; a specific instance of it is described in this previous question on coloring 17x17 grids. One possible approach to individual instances of the problem involves encoding the problem in 4-CNF and running it on a SAT solver.
I'm interested in the current state-of-the-art for SAT solvers (of which I know almost nothing). Specifically, I'm interested in both which algorithm has the largest adoption in practice and WHY (though perhaps less so than the following...), and whether there are recent results that are better purely in terms of complexity. To divorce this as far as possible from any type of specific engineering problem, I'll ask the question in the following form:
What are the current "best" SAT solver algorithms?
Feel free to interpret "best" in the most fitting form. Clickable reference links would be appreciated!
