排序方式: 共有42条查询结果,搜索用时 281 毫秒
1.
2.
David B. Wilson 《Random Structures and Algorithms》2002,21(2):182-195
There has been much recent interest in the satisfiability of random Boolean formulas. A random k‐SAT formula is the conjunction of m random clauses, each of which is the disjunction of k literals (a variable or its negation). It is known that when the number of variables n is large, there is a sharp transition from satisfiability to unsatisfiability; in the case of 2‐SAT this happens when m/n → 1, for 3‐SAT the critical ratio is thought to be m/n ≈ 4.2. The sharpness of this transition is characterized by a critical exponent, sometimes called ν = νk (the smaller the value of ν the sharper the transition). Experiments have suggested that ν3 = 1.5 ± 0.1. ν4 = 1.25 ± 0.05, ν5 = 1.1 ± 0.05, ν6 = 1.05 ± 0.05, and heuristics have suggested that νk → 1 as k → ∞. We give here a simple proof that each of these exponents is at least 2 (provided the exponent is well defined). This result holds for each of the three standard ensembles of random k‐SAT formulas: m clauses selected uniformly at random without replacement, m clauses selected uniformly at random with replacement, and each clause selected with probability p independent of the other clauses. We also obtain similar results for q‐colorability and the appearance of a q‐core in a random graph. © 2002 Wiley Periodicals, Inc. Random Struct. Alg., 21: 182–195, 2002 相似文献
3.
We initiate the study of a new measure of approximation. This measure compares the performance of an approximation algorithm to the random assignment algorithm. This is a useful measure for optimization problems where the random assignment algorithm is known to give essentially the best possible polynomial time approximation. In this paper, we focus on this measure for the optimization problems Max‐Lin‐2 in which we need to maximize the number of satisfied linear equations in a system of linear equations modulo 2, and Max‐k‐Lin‐2, a special case of the above problem in which each equation has at most k variables. The main techniques we use, in our approximation algorithms and inapproximability results for this measure, are from Fourier analysis and derandomization. © 2004 Wiley Periodicals, Inc. Random Struct. Alg., 2004 相似文献
4.
Will Perkins 《Random Structures and Algorithms》2015,47(1):163-173
We study an Achlioptas‐process version of the random k‐SAT process: a bounded number of k‐clauses are drawn uniformly at random at each step, and exactly one added to the growing formula according to a particular rule. We prove the existence of a rule that shifts the satisfiability threshold. This extends a well‐studied area of probabilistic combinatorics (Achlioptas processes) to random CSP's. In particular, while a rule to delay the 2‐SAT threshold was known previously, this is the first proof of a rule to shift the threshold of k‐SAT for . We then propose a gap decision problem based upon this semi‐random model. The aim of the problem is to investigate the hardness of the random k‐SAT decision problem, as opposed to the problem of finding an assignment or certificate of unsatisfiability. Finally, we discuss connections to the study of Achlioptas random graph processes. © 2014 Wiley Periodicals, Inc. Random Struct. Alg., 47, 163–173, 2015 相似文献
5.
Two Solutions to Diluted p-Spin Models and XORSAT Problems 总被引:1,自引:0,他引:1
6.
Jie Wang 《Journal of Complexity》2002,18(4):1024
We present in this paper a dynamic binary coding scheme α on CNF formulas ψ, and show that under a uniform distribution μα on binary string α(ψ), SAT is complete on average, where μα(ψ) is proportional to α(ψ)−22−α(ψ). We then show that there is k0>2 such that for all kk0, kSAT under μα is complete on average. 相似文献
7.
A continuous–discontinuous second‐order transition in the satisfiability of random Horn‐SAT formulas
Cristopher Moore Gabriel Istrate Demetrios Demopoulos Moshe Y. Vardi 《Random Structures and Algorithms》2007,31(2):173-185
We compute the probability of satisfiability of a class of random Horn‐SAT formulae, motivated by a connection with the nonemptiness problem of finite tree automata. In particular, when the maximum clause length is three, this model displays a curve in its parameter space, along which the probability of satisfiability is discontinuous, ending in a second‐order phase transition where it is continuous but its derivative diverges. This is the first case in which a phase transition of this type has been rigorously established for a random constraint satisfaction problem. © 2007 Wiley Periodicals, Inc. Random Struct. Alg., 2007 相似文献
8.
Joachim Mayer Ilse Mitterreiter Franz Josef Radermacher 《Annals of Operations Research》1995,55(1):139-178
Satisfiability problems are of importance for many practical problems. They are NP-complete problems. However, some instances of the SAT problem can be solved efficiently. This paper reports on a study concerning the behaviour of a variety of algorithmic approaches to this problem tested on a set of problems collected at FAW. The results obtained give a lot of insight into the algorithms and problems, yet also show some general technical and methodological problems associated with such comparisons. 相似文献
9.
A Discrete Lagrangian-Based Global-Search Method for Solving Satisfiability Problems 总被引:8,自引:0,他引:8
Satisfiability is a class of NP-complete problems that model a wide range of real-world applications. These problems are difficult to solve because they have many local minima in their search space, often trapping greedy search methods that utilize some form of descent. In this paper, we propose a new discrete Lagrange-multiplier-based global-search method (DLM) for solving satisfiability problems. We derive new approaches for applying Lagrangian methods in discrete space, we show that an equilibrium is reached when a feasible assignment to the original problem is found and present heuristic algorithms to look for equilibrium points. Our method and analysis provides a theoretical foundation and generalization of local search schemes that optimize the objective alone and penalty-based schemes that optimize the constraints alone. In contrast to local search methods that restart from a new starting point when a search reaches a local trap, the Lagrange multipliers in DLM provide a force to lead the search out of a local minimum and move it in the direction provided by the Lagrange multipliers. In contrast to penalty-based schemes that rely only on the weights of violated constraints to escape from local minima, DLM also uses the value of an objective function (in this case the number of violated constraints) to provide further guidance. The dynamic shift in emphasis between the objective and the constraints, depending on their relative values, is the key of Lagrangian methods. One of the major advantages of DLM is that it has very few algorithmic parameters to be tuned by users. Besides the search procedure can be made deterministic and the results reproducible. We demonstrate our method by applying it to solve an extensive set of benchmark problems archived in DIMACS of Rutgers University. DLM often performs better than the best existing methods and can achieve an order-of-magnitude speed-up for some problems. 相似文献
10.
The evolution of SAT algorithms over the last decade has motivated the application of SAT to model checking, initially through the use of SAT in bounded model checking and, more recently, in unbounded model checking. This paper provides an overview of modern SAT algorithms, SAT-based bounded model checking and some of the most promising approaches for unbounded model checking, namely induction and interpolation. Moreover, the paper details a number of techniques that have proven effective in using SAT solvers in model checking. 相似文献