An efficient approach to solving random k-SAT problems

Proving that a propositional formula is contradictory or unsatisfiable is a fundamental task in automated reasoning. This task is coNP-complete. Efficient algorithms are therefore needed when formulae are hard to solve. Random k-SAT formulae provide a test-bed for algorithms because experiments that have become widely popular show clearly that these formulae are consistently difficult for any known algorithm. Moreover, the experiments show a critical value of the ratio of the number of clauses to the number of variables around which the formulae are the hardest on average. This critical value also corresponds to a 'phase transition' from solvability to unsolvability. The question of whether the formulae located around or above this critical value can efficiently be proved unsatisfiable on average ( or even for a. e. formula) remains up to now one of the most challenging questions bearing on the design of new and more efficient algorithms. New insights into this question could indirectly benefit the solving of formulae coming from real-world problems, through a better understanding of some of the causes of problem hardness. In this paper we present a solving heuristic that we have developed, devoted essentially to proving the unsatisfiability of random k-SAT formulae and inspired by recent work in statistical physics. Results of experiments with this heuristic and its evaluation in two recent sat competitions have shown a substantial jump in the efficiency of solving hard, unsatisfiable random k-SAT formulae.