We determine the asymptotical satisfiability probability of a random at-most-k-Horn formula, via a probabilistic analysis of a simple version, called PUR, of positive unit resolution. We show that for $k=k(n)\rightarrow \infty$ the problem can be ``reduced'' to the case k(n)=n, that was solved in cs.DS/9912001. On the other hand, in the case k= a constant the behavior of PUR is modeled by a simple queuing chain, leading to a closed-form solution when $k=2$. Our analysis predicts an ``easy-hard-easy'' pattern in this latter case. Under a rescaled parameter, the graphs of satisfaction probability corresponding to finite values of k converge to the one for the uniform case, a ``dimension-dependent behavior'' similar to the one found experimentally by Kirkpatrick and Selman (Science'94) for k-SAT. The phenomenon is qualitatively explained by a threshold property for the number of iterations of PUR makes on random satisfiable Horn formulas.

翻译：我们通过分析一种称为PUR（正单元归结）的简化版本的概率性质，确定了随机至多k-Horn公式的渐近可满足概率。研究表明，当 $k=k(n)\rightarrow \infty$ 时，该问题可"归约"至已由cs.DS/9912001解决的k(n)=n情形。另一方面，当k为常数时，PUR的行为可由简单排队链建模，并在 $k=2$ 时得到闭式解。我们的分析预测了后一情形中存在的"易-难-易"模式。在重标度参数下，有限k值对应的可满足概率曲线收敛于均匀情形的曲线，这种"维度依赖行为"与Kirkpatrick和Selman（Science'94）在k-SAT实验中观察到的现象相似。该现象可通过PUR在随机可满足Horn公式上的迭代次数阈值特性进行定性解释。