BriefGPT.xyz
Jun, 2022
命题公式是否难以证明?
Are Hitting Formulas Hard for Resolution?
HTML
PDF
Tomáš Peitl, Stefan Szeider
TL;DR
本文研究打击公式的可满足性和分辨率复杂性,确定不可化简打击公式来确定其分辨率复杂性,并使用 Nauty 软件包枚举其精确的分辨率复杂性等。
Abstract
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
→