On the limit of branching rules for hard random unsatisfiable 3-SAT Original Research Article

We study the limit of branching rules in the Davis–Logemann–Loveland (DLL) procedure for hard random unsatisfiable 3-SAT and try to answer the question: what would be the search tree size if every branching variable were the best possible? The issue is of practical interest because much effort has been spent in designing better branching rules. Our experimental results suggest that the branching rules used in the current state-of-the-art DLL procedures are probably already close to the optimal for hard random unsatisfiable 3-SAT, and in particular, that the first of the 10 challenges for propositional reasoning and search formulated by Selman et al. (Proceedings of IJCAI-97, Nagoya, Aichi, Japan, August 1997), namely, proving that a hard 700 variable random 3-SAT formula is unsatisfiable, should be very difficult to answer by a DLL procedure unless something significantly different from branching can be made effective for hard random unsatisfiable 3-SAT.