I've read the paper fairly closely, and it mostly seems like the author is hiding a conflict-driven search in ill-stated data structures, which allow him to perform a faulty analysis of the runtime of his algorithm.<p>I've implemented a SAT solver and read the literature extensively. This paper is not up the standards of clarity imposed by that literature, see, eg, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver" (Zhang, available for free online). There is a world of difference in the clarity of presentation between these two papers. There might be an English language barrier problem operating, I don't know.<p>If the author did some work to polish his presentation and state definitions more clearly, as well as submit his SAT solver to well know competitions, (<a href="http://www.satcompetition.org/2011/" rel="nofollow">http://www.satcompetition.org/2011/</a>), I'm sure he could get some attention from the relevant people. Given how clear it looks right now, I'm too busy with my own research to try and pull out the hidden conflict-driven algorithm that I suspect exists in this paper, as it would be very time-consuming for little expected gain on my end.<p>If his algorithm beats the pants off all the others in SAT 2011, well, then I'd get right down to work.<p>Homework for someone who has some time: download his code and make it run on SAT 2010. Compare to other algorithms from that competition. Not, of course, a definitive test, but it it performs even in the middle of the pack, then you'll know it is worth a closer look.