We study from the proof complexity perspective the (informal) proof search problem:
Is there an optimal way to search for propositional proofs?
We note that for any fixed proof system there exists a time-optimal proof search algorithm. Using classical proof complexity results about reflection principles we prove that a time-optimal proof search algorithm exists without restricting proof systems iff a p-optimal proof system exists.
To characterize precisely the time proof search algorithms need for individual formulas we introduce a new proof complexity measure based on algorithmic information concepts. In particular, to a proof system $P$ we attach {\bf information-efficiency function} $i_P(τ)$ assigning to a tautology a natural number, and we show that:
- $i_P(τ)$ characterizes time any $P$-proof search algorithm has to use on $τ$ and that for a fixed $P$ there is such an information-optimal algorithm,
- a proof system is information-efficiency optimal iff it is p-optimal,
- for non-automatizable systems $P$ there are formulas $τ$ with short proofs but having large information measure $i_P(τ)$.
We isolate and motivate the problem to establish unconditional super-logarithmic lower bounds for $i_P(τ)$ where no super-polynomial size lower bounds are known. We also point out connections of the new measure with some topics in proof complexity other than proof search.
Short Propositional Refutations for Dense Random 3CNF Formulas
随机3CNF公式是衡量命题证明系统平均情况行为的重要分布。许多命题证明系统中随机3CNF反驳的下界是已知的。最值得注意的是带有$Ω(n^{1.5-ε}) $子句的随机3CNF公式的指数大小分辨率反驳下界[Chvatal and Szemeredi（1988），Ben-Sasson and Wigderson（2001）]。另一方面，在非抽象命题证明系统中，关于随机3CNF反驳的大小的唯一已知的非平凡上界是用于$Ω(n^{2}/\log n) $子句的归结，由Beame等人（2002）示出。在本文中，我们表明，已经标准的命题证明系统，弗雷格证明层次内，承认短期反驳随机3CNF公式，足够大的条款变量比。具体来说，我们证明多项式大小的命题反驳，其行是$TC^0$公式（即，$TC^0$ -Frege证明），用于具有$ n $变量和$ Ω(n^{1.4}) $子句的随机3CNF公式。这个想法是基于Feige，Kim和Ofek（2006）给出的随机3CNF不可满足性证明的有效命题正确性证明。由于这些证人的可靠性是使用频谱技术验证，我们开发了一个适当的方式来推理命题系统中的特征向量。为了进行充分的论证，我们在弱形式算术系统中工作，并使用一般的翻译方案来证明命题。
