Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark contrast with other polynomial-time decidable classes, which usually have algorithms based on backtracking and resolution and for which model counting remains hard, like 2-SAT and Horn-SAT. However, those resolution-based algorithms usually easily imply an upper bound on resolution complexity, which is missing for hitting formulas. Are hitting formulas hard for resolution? In this paper we take the first steps towards answering this question. We show that the resolution complexity of hitting formulas is dominated by so-called irreducible hitting formulas, first studied by Kullmann and Zhao, that cannot be composed of smaller hitting formulas. However, by definition, large irreducible unsatisfiable hitting formulas are difficult to construct; it is not even known whether infinitely many exist. Building upon our theoretical results, we implement an efficient algorithm on top of the Nauty software package to enumerate all irreducible unsatisfiable hitting formulas with up to 14 clauses. We also determine the exact resolution complexity of the generated hitting formulas with up to 13 clauses by extending a known SAT encoding for our purposes. Our experimental results suggest that hitting formulas are indeed hard for resolution.
翻译:由 Iwama 介绍的命中公式是非同寻常的平面 CNF 公式。 不仅在多民族时代, 其相对性可降解的公式是非常规的, 甚至它们的模型也可以以封闭的形式计算。 这与其他多边- 多边- 时间衰减的公式形成鲜明对比, 后者通常有基于回溯和解析的算法, 而对于这些公式, 其模型的计算仍然很困难, 比如 2SAT 和 Horn- SAT 。 然而, 这些基于分辨率的算法通常很容易意味着对分辨率复杂性的上限, 而击出公式时却缺少。 在本文中,我们为解决这个问题采取了最初的步骤。 我们显示, 击中公式的解析复杂性是由所谓的不可减损的调制式公式所决定的。 由库尔曼 和赵 首次研究的这些公式不能由较小的打击公式组成。 但是, 定义上, 大量不可降低的不满意度的打击公式是难以构建的; 甚至不知道是否存在无限的公式。 根据我们的理论结果, 我们用一个有效的算法, 将一个有效的算法的计算方法在顶端端端端端端端端上, 我们的公式, 将13号的公式的精确地推到了我们无法理解的公式。