AI 中文总结
该研究定义蓝色 pebbling 代价，精确刻画树形与负归结的空间界，证明两类归结的空间分离，并改进现有相关刻画结果。
AI 中文摘要
红-蓝 pebble 游戏是一种知名的图上双人游戏，过去曾被用作分析多种计算模型及证明系统中复杂度度量的工具。我们定义了一种新的游戏代价度量：蓝色代价，仅统计游戏过程中被标记为蓝色的 pebble 数量。这一新度量可精确刻画树形与负归结中的若干空间界。特别地，我们证明对于任意不可满足公式 F，该公式在树形归结中的子句空间需求，与在 F 的反驳图（不一定为树）上进行游戏的最小蓝色 pebbling 代价完全一致。这一结果与基于标准黑色 pebble 游戏的一般归结已知结果完全对应，且改进了现有基于可逆 pebbling 的树形空间近似刻画。我们还证明蓝色 pebbling 代价也适用于分析提升 pebble 公式 Peb_G[∨] 和 Peb_G[⊕] 在两种归结限制下的空间需求：在树形归结中，Peb_G[∨] 的子句空间与底层图 G 的蓝色代价渐近一致；在负归结中，我们对两类提升公式的空间得到了几乎匹配的上界和下界，与一般归结现有结果类似。我们还证明了树形归结与负归结之间的近最优空间分离：给出一类含 n 个变量的公式，其在负归结中需要 Ω(n/log n) 的子句空间，但存在常数空间的树形归结反驳。这与负归结可仅以规模小幅增长模拟树形归结的事实形成对比。
英文摘要
The red-blue pebble game is a well known two-player game on graphs that has been used in the past as a tool to analyze complexity measures in several computation models as well as proof systems. We define a new way to measure the cost of the game, the blue cost, which only counts the number of pebbles that are colored blue during the game. This new measure characterizes exactly several space bounds in tree-like and negative Resolution. In particular we prove that for any unsatiafiable formula $F$, the clause space requirements of the formula in tree-like Resolution, exactly coincide with the minimum blue pebbling cost of the game played on a refutation graph of $F$ (not necessarily a tree). This exactly parallels the known result for general Resolution in terms of the standard black pebble game, and improves the existing approximated characterization of tree-like space in terms of reversible pebbling. We show that the blue pebbling cost is also well suited for analyzing the space requirements of the lifted pebbling formulas $Peb_G[\vee]$ and $Peb_G[\oplus]$ in the two Resolution restrictions. In the case of tree-like Resolution, the clause space of $Peb_G[\vee]$ asymptotically coincides with the blue cost of the underlying graph $G$. For the case of negative Resolution, we obtain almost matching upper and lower bounds for the space in the two classes of lifted formulas, similar to the ones existing for general Resolution. We also prove a close to optimal space separation between tree-like and negative Resolution, presenting a class of formulas with $n$ variables that require clause space $Ω(\frac{n}{\log n})$ in negative Resolution, but have constant space tree-like refutations. This contrasts with the fact that negative Resolution can simulate tree-like Resolution with only a small increase in size.
