In this paper we generalize a heuristic that we have introduced previously for solving efficiently random 3-SAT formulae. Our heuristic is based on the notion of backbone, searching variables belonging to local backbones of a formula. This heuristic was limited to 3-SAT formulae. In this paper we generalize this heuristic by introducing a sub-heuristic called a re-normalization heuristic in order to handle formulae with various clause lengths and particularly hard random k-SAT formulae with k ≥ 3. We implemented this new general heuristic in our previous program cnfs, a classical dpll algorithm, renamed kcnfs, We give experimental results which show that kcnfs outperforms by far the best current complete solvers on any random k-SAT formula for k ≥ 3.
展开▼
