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.
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.
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, (http://www.satcompetition.org/2011/), 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.
If his algorithm beats the pants off all the others in SAT 2011, well, then I'd get right down to work.
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.
I would like to clarify that just because an algorithm runs slower than the ones used by solvers in competitions like SAT, it doesn't mean much, as we're looking at asymptotic complexity here. To give an example: the "PRIMES is in P" paper gives a poly time algorithm to determine if a given number is prime or not, but in practice, it runs slower than tests like probabilistic algorithms like Miller-Rabin.
Very true, I'm sorry if I implied otherwise above. However, using a well-known SAT benchmark to assess correctness/performance in the absence of a clearer statement of the algorithm would still be a good step to take, if someone was interested.
"To give an example: the "PRIMES is in P" paper gives a poly time algorithm to determine if a given number is prime or not, but in practice, it runs slower than tests like probabilistic algorithms like Miller-Rabin."
I agree in principle, but the example is a bad one. Here, a deterministic polynomial time algorithm is stacked against probabilistic polynomial time algorithms.
In SAT, we'd have the (hypothetically) polynomial algorithm against exponential time algorithms. Theoretically, the constants in the polynomial might of course be so large as to erase the advantage on non-galactic problem sizes but this happens rarely.
Another example is Linear Programming - it is provably polynomial using the ellipsoid algorithm but people tend to use algorithms (such as simplex) which are not provably in P but run much faster in practice.
The problem with the ellipsoid method is not speed but rather numerical stability. It would work great if we only had "real reals", i.e. reals with infinite precision.
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.
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, (http://www.satcompetition.org/2011/), 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.
If his algorithm beats the pants off all the others in SAT 2011, well, then I'd get right down to work.
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.