Hiding Satisfying Satisfacing:我的第一次
Hiding Satisfying Assignments: Two are Better than One
摘要:
不完全可满足性求解器的评价关键取决于硬可满足实例的可用性。这种情况的一个合理来源是随机k-SAT公式,其子句是从满足某个随机选择的真值分配A的所有子句中均匀选择的。不幸的是,以这种方式生成的实例往往相对容易,并且可以通过实际的算法有效地解决。粗略地说,随着公式密度的增加,对于许多不同的算法,A充当越来越强的吸引子。最近的结果的空间上的几何满足随机k-SAT和NAE-k-SAT公式的真理分配的启发,我们介绍了一个简单的扭曲这个基本模型,这似乎大大增加了它的硬度。也就是说,除了禁止被隐藏赋值A违反的子句外,我们还禁止被它的补语违反的子句,使得A和A的补语都是令人满意的。似乎在这种“对称化”下,两个吸引子的影响在很大程度上抵消了,使得算法更难找到任何真值分配。我们给出了支持这一论断的理论和实验证据。
英文摘要:
The evaluation of incomplete satisfiability solvers depends critically on the availability of hard satisfiable instances. A plausible source of such instances consists of random k-SAT formulas whose clauses are chosen uniformly from among all clauses satisfying some randomly chosen truth assignment A. Unfortunately, instances generated in this manner tend to be relatively easy and can be solved efficiently by practical heuristics. Roughly speaking, as the formula's density increases, for a number of different algorithms, A acts as a stronger and stronger attractor. Motivated by recent results on the geometry of the space of satisfying truth assignments of random k-SAT and NAE-k-SAT formulas, we introduce a simple twist on this basic model, which appears to dramatically increase its hardness. Namely, in addition to forbidding the clauses violated by the hidden assignment A, we also forbid the clauses violated by its complement, so that both A and complement of A are satisfying. It appears that under this "symmetrization'' the effects of the two attractors largely cancel out, making it much harder for algorithms to find any truth assignment. We give theoretical and experimental evidence supporting this assertion.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。