通过欺骗性隐藏解生成硬可满足公式
Generating Hard Satisfiable Formulas by Hiding Solutions Deceptively
摘要：
为了测试约束满足问题（如3-SAT）的不完全搜索算法，我们需要一个硬的、但可满足的基准实例源。一个简单的方法是选择一个随机的真值赋值A，然后从A满足的子句中随机选择子句。然而，这种方法往往会产生简单的问题，因为大多数文字都指向“隐藏的”赋值A。去年，Achlioptas，Jia和Moore提出了一个问题生成器，通过隐藏A及其补数来消除这种影响。虽然所得公式对于DPLL算法来说似乎与没有隐藏分配的随机3-SAT公式一样困难，但它们可以通过WalkSAT仅在多项式时间内求解。在这里，我们提出了一种新的方法来消除对A的吸引力，通过选择一个子句，其中t > 0的文字满足A，概率与q^t成比例，其中q < 1。通过改变q，我们可以生成变量没有偏差的公式，即，它们是真或假的可能性相等;我们甚至可以使公式“欺骗性地”指向远离A的地方。我们目前的理论和实验结果表明，这些公式是指数硬DPLL算法和不完整的算法，如WalkSAT。
英文摘要：
To test incomplete search algorithms for constraint satisfaction problems such as 3-SAT, we need a source of hard, but satisfiable, benchmark instances. A simple way to do this is to choose a random truth assignment A, and then choose clauses randomly from among those satisfied by A. However, this method tends to produce easy problems, since the majority of literals point toward the ``hidden'' assignment A. Last year, Achlioptas, Jia and Moore proposed a problem generator that cancels this effect by hiding both A and its complement. While the resulting formulas appear to be just as hard for DPLL algorithms as random 3-SAT formulas with no hidden assignment, they can be solved by WalkSAT in only polynomial time. Here we propose a new method to cancel the attraction to A, by choosing a clause with t > 0 literals satisfied by A with probability proportional to q^t for some q < 1. By varying q, we can generate formulas whose variables have no bias, i.e., which are equally likely to be true or false; we can even cause the formula to ``deceptively'' point away from A. We present theoretical and experimental results suggesting that these formulas are exponentially hard both for DPLL algorithms and for incomplete algorithms such as WalkSAT.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
