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 条

[1] An Efficient Approach to Solving Random k-sat Problems
Gilles Dequen
Olivier Dubois
Journal of Automated Reasoning, 2006, 37 : 261 - 276
[2] An efficient approach to solving random k-SAT problems
Dequen, Gilles
Dubois, Olivier
JOURNAL OF AUTOMATED REASONING, 2006, 37 (04) : 261 - 276
[3] The backtracking survey propagation algorithm for solving random K-SAT problems
Raffaele Marino
Giorgio Parisi
Federico Ricci-Tersenghi
Nature Communications, 7
[4] The backtracking survey propagation algorithm for solving random K-SAT problems
Marino, Raffaele
Parisi, Giorgio
Ricci-Tersenghi, Federico
NATURE COMMUNICATIONS, 2016, 7
[5] Solving k-SAT problems with generalized quantum measurement
Zhang, Yipei
Lewalle, Philippe
Whaley, K. Birgitta
arXiv,
[6] kcnfs:: An efficient solver for random k-SAT formulae
Dequen, G
Dubois, O
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2004, 2919 : 486 - 501
[7] Polarised random k-SAT
Danielsson, Joel Larsson
Markstrom, Klas
COMBINATORICS PROBABILITY AND COMPUTING, 2023, 32 (06) : 885 - 899
[8] Biased random k-SAT
Larsson, Joel
Markstrom, Klas
RANDOM STRUCTURES & ALGORITHMS, 2021, 59 (02) : 238 - 266
[9] On an online random k-SAT model
Kravitz, David
RANDOM STRUCTURES & ALGORITHMS, 2008, 32 (01) : 115 - 124
[10] On the behaviour of random K-SAT on trees
Krishnamurthy, Supriya
Sumedha
JOURNAL OF STATISTICAL MECHANICS-THEORY AND EXPERIMENT, 2012,

← 1 2 3 4 5 →