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

共 50 条

[31] A novel weighting scheme for random k-SAT关于随机 k-SAT 的新加权方法
Jun Liu
Ke Xu
Science China Information Sciences, 2016, 59
[32] Random k-SAT:: A tight threshold for moderately growing k
Frieze, A
Wormald, NC
COMBINATORICA, 2005, 25 (03) : 297 - 305
[33] Random k-Sat: A Tight Threshold For Moderately Growing k
Alan Frieze*
Nicholas C. Wormald†
Combinatorica, 2005, 25 : 297 - 305
[34] Regular Random k-SAT: Properties of Balanced Formulas
Yacine Boufkhad
Olivier Dubois
Yannet Interian
Bart Selman
Journal of Automated Reasoning, 2005, 35 : 181 - 200
[35] On belief propagation guided decimation for random k-SAT
Coja-Oghlan, Amin
Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, 2011, : 957 - 966
[36] On Belief Propagation Guided Decimation for Random k-SAT
Coja-Oghlan, Amin
PROCEEDINGS OF THE TWENTY-SECOND ANNUAL ACM-SIAM SYMPOSIUM ON DISCRETE ALGORITHMS, 2011, : 957 - 966
[37] The high temperature case for the random K-sat problem
Michel Talagrand
Probability Theory and Related Fields, 2001, 119 : 187 - 212
[38] The high temperature case for the random K-sat problem
Talagrand, M
PROBABILITY THEORY AND RELATED FIELDS, 2001, 119 (02) : 187 - 212
[39] Regular random k-SAT:: Properties of balanced formulas
Boufkhad, Yacine
Dubois, Olivier
Interian, Yannet
Selman, Bart
JOURNAL OF AUTOMATED REASONING, 2005, 35 (1-3) : 181 - 200
[40] Complexity of k-SAT
Impagliazzo, R
Paturi, R
FOURTEENTH ANNUAL IEEE CONFERENCE ON COMPUTATIONAL COMPLEXITY, PROCEEDINGS, 1999, : 237 - 240

← 1 2 3 4 5 →