检索结果-内蒙古大学图书馆

Short propositional refutations for dense random 3CNF formulas

ANNALS OF PURE AND APPLIED LOGIC 2014年第12期165卷 1864-1918页

作者： Mueller, Sebastian Tzameret, Iddo Natl Inst Informat Tokyo Japan Univ London Dept Comp Sci London WC1E 7HU England

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Omega(n(1.5-epsilon)) clauses (Chvatal and Szemeredi [14], Ben-Sasson and Wigderson [10]). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Omega(n(2)/log n) clauses, shown by Beame et al. [6]. In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables and Omega(n(1.4)) clauses. The idea is based on demonstrating efficient propositional correctness proofs of the random 3CNF unsatisfiability witnesses given by Feige, Kim and Ofek [23]. Since the soundness of these witnesses is verified using spectral techniques, we develop an appropriate way to reason about eigenvectors in propositional systems. To carry out the full argument we work inside weak formal systems of arithmetic and use a general translation scheme to propositional proofs. (C) 2014 Elsevier B.V. All rights reserved.

关键词： Propositional proof complexity Random 3-SAT refutation algorithms Threshold logic Frege proofs

来源：评论

学校读者我要写书评

暂无评论

Short Propositional refutations for Dense Random 3CNF Formulas 12

Short Propositional Refutations for Dense Random 3CNF Formul...

引用

27th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

作者： Mueller, Sebastian Tzameret, Iddo Charles Univ Prague Fac Math & Phys Prague Czech Republic Tsinghua Univ IIIS Inst Theoret Comp Sci Beijing Peoples R China

ISBN: (纸本)9780769547695

Random 3CNF formulas constitute an important distribution for measuring the average-case behavior of propositional proof systems. Lower bounds for random 3CNF refutations in many propositional proof systems are known. Most notable are the exponential-size resolution refutation lower bounds for random 3CNF formulas with Omega(n(1.5-epsilon)) clauses (Chvatal and Szemeredi [13], Ben-Sasson and Wigderson [9]). On the other hand, the only known non-trivial upper bound on the size of random 3CNF refutations in a non-abstract propositional proof system is for resolution with Omega(n(2)/log n) clauses, shown by Beame et al. [5]. In this paper we show that already standard propositional proof systems, within the hierarchy of Frege proofs, admit short refutations for random 3CNF formulas, for sufficiently large clause-to-variable ratio. Specifically, we demonstrate polynomial-size propositional refutations whose lines are TC0 formulas (i.e., TC0-Frege proofs) for random 3CNF formulas with n variables and Omega(n(1.4)) clauses. The idea is based on demonstrating efficient propositional correctness proofs of the random 3CNF unsatisfiability witnesses given by Feige, Kim and Ofek [19]. Since the soundness of these witnesses is verified using spectral techniques, we develop an appropriate way to reason about eigenvectors in propositional systems. To carry out the full argument we work inside weak formal systems of arithmetic and use a general translation scheme to propositional proofs.

关键词： Proof complexity random 3-SAT refutation algorithms threshold logic Frege proofs

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：