An efficient approach to solving random k-sat problems

被引：0

作者：

Dequen, Gilles ^{[1
]}

Dubois, Olivier ^{[2
]}

机构：

[1] LaRIA, Université de Picardie Jules Verne, 33 Rue St Leu, 80039 Amiens Cedex 1, France

[2] LIP6, CNRS-Université Paris 6, 4 place Jussieu, 75252 Paris Cedex 05, France

来源：

Journal of Automated Reasoning | 2006年 / 37卷 / 04期

关键词：

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 kSAT 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 kSAT 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 kSAT sat formulae. © Springer Science+Business Media; Inc; 2007;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

Journal article (JA)

引用

页码：261 / 276