Minimum propositional proof length is NP-hard to linearly approximate
Minimum propositional proof length is NP-hard to linearly approximate
复制标题
最小命题证明长度是 NP 难线性近似的
DOI：
10.2307/2694916
复制
发表时间：
1998
影响因子：
0.6
通讯作者：
T. Pitassi
中科院分区：
文献类型：
--
作者：
Michael Alekhnovich;S. Buss;S. Moran;T. Pitassi
摘要 我们证明确定最小命题证明长度的问题是 NP 困难的，难以在 的因子内近似。这些结果非常稳健，因为它们适用于几乎所有自然证明系统，包括：弗雷格系统、扩展弗雷格系统、分辨率。 Horn 解析、多项式微积分、序列微积分、无割序列微积分以及多项式微积分。我们的近似结果硬度通常适用于通过符号数量或推理数量测量的证明长度，用于树状或DAG状证明。我们引入单调最小（电路）满足分配问题并将其简化为证明长度的近似问题。
Abstract We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.