小内存条件下DPLL算法的硬可满足公式
Hard satisfiable formulas for DPLL algorithms using heuristics with small memory
摘要：
求解布尔可满足性问题（SAT）的DPLL算法可以表示为一个过程的形式，该过程使用算法$A$和$B$，从输入公式$φ$和值$b$中选择变量$x$，并在公式$φ[x := b]$和$φ[x := 1 - b]$上递归运行。不可满足公式上的DPLL算法的运行时间的指数下界来自树状分辨率证明的下界。可满足公式的下限对于某些类别的DPLL算法（诸如“近视”和“醉酒”算法）也是已知的。所有的下限都是针对DPLL算法的类别，这些算法限制了算法对公式的访问。在本文中，我们认为DPLL算法与算法，有无限的访问公式，但使用小内存。我们表明，对于任何一对小内存的算法存在一个家庭的可满足的公式$Φ_n$，这样的DPLL算法，使用这些算法在指数时间运行的公式$Φ_n$。
英文摘要：
DPLL algorithm for solving the Boolean satisfiability problem (SAT) can be represented in the form of a procedure that, using heuristics $A$ and $B$, select the variable $x$ from the input formula $φ$ and the value $b$ and runs recursively on the formulas $φ[x := b]$ and $φ[x := 1 - b]$. Exponential lower bounds on the running time of DPLL algorithms on unsatisfiable formulas follow from the lower bounds for tree-like resolution proofs. Lower bounds on satisfiable formulas are also known for some classes of DPLL algorithms such as "myopic" and "drunken" algorithms. All lower bounds are made for the classes of DPLL algorithms that limit heuristics access to the formula. In this paper we consider DPLL algorithms with heuristics that have unlimited access to the formula but use small memory. We show that for any pair of heuristics with small memory there exists a family of satisfiable formulas $Φ_n$ such that a DPLL algorithm that uses these heuristics runs in exponential time on the formulas $Φ_n$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
