A Wealth of SAT Distributions with Planted Assignments
A Wealth of SAT Distributions with Planted Assignments
复制标题
大量 SAT 分配以及已安排的作业
DOI：
10.1007/978-3-540-45193-8_19
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
T. Dimitriou
中科院分区：
文献类型：
--
作者：
T. Dimitriou
约束满足和可满足性问题的局部搜索算法的评价是基于保证可满足的实例的生成。一种流行的创建硬可满足实例的方法是使用完全搜索过程来过滤掉不可满足的实例。然而，这种方法有两个问题;第一，产生的实例的大小是有限的，第二，产生的实例是远远不是随机的。虽然可以产生满意的实例，通过减少某些计算问题SAT，它是不知道如何可以直接fork-SAT开发一个类似的生成器。在这项工作中，我们提供了一个生成器的anoptimizationversion的k-SAT，具有一定的有用的属性。首先，我们展示了如何产生加权的MAXk-SAT实例，其中一个寻求最大化满足条款的权重。其次，我们提供了一个很好的表征的最优解;在我们的模型中，我们不仅知道如何最优解看起来像，但我们也证明它是唯一的。最后，我们表明，我们的发电机hastunable复杂性，通过适当地选择参数，可以控制所生成的实例的硬度，导致一个简单的硬容易的模式，在搜索复杂性良好的分配和一种新型的相变。
Evaluation of local search heuristics for constraint satisfaction and satisfiability problems is based on the generation of instances that are guaranteed to be satisfiable. One popular method for creating hard satisfiable instances is the use ofcompletesearch procedures to filter out unsatisfiable instances. This approach however has two problems; first, the size of instances produced is limited considerably and second, the generated instances are far from being random.Although one can generate satisfiable instances by reducing certain computational problems to SAT, it is not known how a similar generator can be developeddirectlyfork-SAT. In this work we provide a generator for anoptimizationversion ofk-SAT that has certain useful properties. First, we show how to produce weighted instances of MAXk-SAT where one seeks to maximize theweightof satisfied clauses. Second, we provide a nice characterization of the optimal solution; in our model not only we know how the optimal solution looks like but we also prove it isunique. Finally, we show that our generator hastunable complexity; by appropriately choosing parameters one can control the hardness of the generated instances leading to an easy-hard-easy pattern in the search complexity for good assignments and a new type of phase transition.