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

Pseudorandom generators in propositional proof complexity

SIAM JOURNAL ON COMPUTING 2004年第1期34卷 67-88页

作者： Alekhnovich, M Ben-Sasson, E Razborov, AA Wigderson, A Moscow MV Lomonosov State Univ Moscow Russia Hebrew Univ Jerusalem Inst Comp Sci Jerusalem Israel VA Steklov Math Inst Moscow 117333 Russia Inst Adv Study Princeton NJ 08540 USA

We call a pseudorandom generator G(n) : {0, 1}(n) --> {0, 1}(m) hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement G(n)(x(1),..., x(n)) not equal b for any string b is an element of{0, 1}(m). We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as resolution, polynomial calculus, and polynomial calculus with resolution (PCR).

关键词： generator propositional proof complexity resolution polynomial calculus

来源：评论

学校读者我要写书评

暂无评论

Lower bounds for Lovasz-Schrijver systems and beyond follow from multiparty communication complexity

引用

SIAM JOURNAL ON COMPUTING 2007年第3期37卷 845-869页

作者： Beame, Paul Pitassi, Toniann Segerlind, Nathan Univ Washington Seattle WA 98195 USA Univ Toronto Dept Comp Sci Toronto ON M5S 1A4 Canada Portland State Univ Dept Comp Sci Portland OR 97207 USA

We prove that an omega (log(4) n) lower bound for the three- party number- on- the- forehead ( NOF) communication complexity of the set- disjointness function implies an n.( 1) size lower bound for treelike Lovasz - Schrijver systems that refute unsatisfiable formulas in conjunctive normal form (CNFs). More generally, we prove that an n(Omega(1)) lower bound for the ( k + 1)- party NOF communication complexity of set disjointness implies a 2(n Omega(1)) size lower bound for all treelike proof systems whose formulas are degree k polynomial inequalities.

关键词： propositional proof complexity zero-one programming communication complexity lower bounds

来源：评论

学校读者我要写书评

暂无评论

proof complexity AND THE BINARY ENCODING OF COMBINATORIAL PRINCIPLES

引用

SIAM JOURNAL ON COMPUTING 2024年第3期53卷 764-802页

作者： Dantchev, Stefan Galesi, Nicola Ghani, Abdul Martin, Barnaby Univ Durham Dept Comp Sci Durham England Sapienza Univ Roma Dipartimento Ingn Informat Automat & Gest A Rubert Rome Italy

We consider proof complexity in light of the unusual binary encoding of certain combinatorial principles. We contrast this proof complexity with the normal unary encoding in several refutation systems, based on Resolution and Sherali-Adams. We first consider Res(s), which is an extension of Resolution working on s-DNFs (Disjunctive Normal Form formulas). We prove an exponential lower bound of n(Omega(k)/d(s)) for the size of refutations of the binary version of the k-Clique Principle in Res(s), where s = o ((log log n)(1/3)) and d(s) is a doubly exponential function. Our result improves that of Lauria et al., who proved a similar lower bound for Res(1), i.e., Resolution. For the k-Clique and other principles we study, we show how lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for the binary version, so we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the (weak) Pigeonhole Principle Bin-PHPnm. We prove that for any delta, epsilon > 0, Bin-PHPnm requires refutations of size 2(n1-delta) in Res(s) for s = O(log(1/2-epsilon) n). Our lower bound cannot be improved substantially with the same method since for m >= 2(root n) (log) (n) we can prove there are 2(O) ((root n) (log) (n)) size refutations of Bin-PHPnm in Res (log n). This is a consequence of the same upper bound for the unary weak Pigeonhole Principle of Buss and Pitassi. We contrast unary versus binary encoding in the Sherali-Adams (SA) refutation system where we prove lower bounds for both rank and size. For the unary encoding of the Pigeonhole Principle and the Ordering Principle, it is known that linear rank is required for refutations in SA, although both admit refutations of polynomial size. We prove that the binary encoding of the (weak) Pigeonhole Principle Bin-PHPnm requires exponentially sized (in n) SA refutations, whereas th

关键词： propositional proof complexity resolution lift-and-project methods Sherali-Adams binary encoding

来源：评论

学校读者我要写书评

暂无评论

On Optimal Heuristic Randomized Semidecision Procedures, with Applications to proof complexity and Cryptography

引用

THEORY OF COMPUTING SYSTEMS 2012年第2期51卷 179-195页

作者： Hirsch, Edward A. Itsykson, Dmitry Monakhov, Ivan Smal, Alexander VA Steklov Math Inst St Petersburg 191011 Russia

The existence of an optimal propositional proof system is a major open question in proof complexity;many people conjecture that such systems do not exist. Krajiek and Pudlak (J. Symbol. Logic 54(3):1063, 1989) show that this question is equivalent to the existence of an algorithm that is optimal on all propositional tautologies. Monroe (Theor. Comput. Sci. 412(4-5):478, 2011) recently presented a conjecture implying that such an algorithm does not exist. We show that if one allows errors, then such optimal algorithms exist. The concept is motivated by the notion of heuristic algorithms. Namely, we allow an algorithm, called a , to claim a small number of false "theorems" and err with bounded probability on other inputs. The amount of false "theorems" is measured according to a polynomial-time samplable distribution on non-tautologies. Our result remains valid for all recursively enumerable languages and can also be viewed as the existence of an optimal weakly automatizable heuristic proof system. The notion of a heuristic acceptor extends the notion of a classical acceptor;in particular, an optimal heuristic acceptor for any distribution simulates every classical acceptor for the same language. We also note that the existence of a --language with a polynomial-time samplable distribution on that has no polynomial-time heuristic acceptors is equivalent to the existence of an infinitely-often one-way function.

关键词： propositional proof complexity Optimal algorithm Infinitely-often one-way

来源：评论

学校读者我要写书评

暂无评论

Parameterized proof complexity

引用

COMPUTATIONAL complexity 2011年第1期20卷 51-85页

作者： Dantchev, Stefan Martin, Barnaby Szeider, Stefan Univ Durham Dept Comp Sci Durham DH1 3LE England

We propose a proof-theoretic approach for gaining evidence that certain parameterized problems are not fixed-parameter tractable. We consider proofs that witness that a given propositional formula cannot be satisfied by a truth assignment that sets at most k variables to true, considering k as the parameter (we call such a formula a parameterized contradiction). One could separate the parameterized complexity classes FPT and W[SAT] by showing that there is no fpt-bounded parameterized proof system for parameterized contradictions, i.e., that there is no proof system that admits proofs of size f(k)n (O(1)) where f is a computable function and n represents the size of the propositional formula. By way of a first step, we introduce the system of parameterized tree-like resolution and show that this system is not fpt-bounded. Indeed, we give a general result on the size of shortest tree-like resolution proofs of parameterized contradictions that uniformly encode first-order principles over a universe of size n. We establish a dichotomy theorem that splits the exponential case of Riis's complexity gap theorem into two subcases, one that admits proofs of size f(k)n (O(1)) and one that does not. We also discuss how the set of parameterized contradictions may be embedded into the set of (ordinary) contradictions by the addition of new axioms. When embedded into general (DAG-like) resolution, we demonstrate that the pigeonhole principle has a proof of size 2 (k) n (2). This contrasts with the case of tree-like resolution where the embedded pigeonhole principle falls into the "non-FPT" category of our dichotomy.

关键词： propositional proof complexity parameterized complexity complexity gap theorems

来源：评论

学校读者我要写书评

暂无评论

A complexity gap for tree resolution

引用

COMPUTATIONAL complexity 2001年第3期10卷 179-209页

作者： Riis, S Univ London Dept Comp Sci London E1 4NS England

This paper shows that any sequence psi(n) of tautologies which expresses the validity of a fixed combinatorial principle either is "easy", i.e. has polynomial size tree-resolution proofs, or is "difficult", i.e. requires exponential size tree-resolution proofs. It is shown that the class of tautologies which are hard (for tree resolution) is identical to the class of tautologies which are based on combinatorial principles which are violated for infinite sets. Further it is shown that the gap phenomenon is valid for tautologies based on infinite mathematical theories (i.e. not just based on a single proposition). A corollary to this classification is that it is undecidable whether a sequence psi(n) has polynomial size tree-resolution proofs or requires exponential size tree-resolution proofs. It also follows that the degree of the polynomial in the polynomial size (in case it exists) is non-recursive, but semi-decidable.

关键词： logical aspects of complexity propositional proof complexity resolution proofs

来源：评论

学校读者我要写书评

暂无评论

Rank complexity gap for Lovasz-Schrijver and Sherali-Adams proof systems

引用

COMPUTATIONAL complexity 2013年第1期22卷 191-213页

作者： Dantchev, Stefan Martin, Barnaby Univ Durham Sch Engn & Comp Sci Durham DH1 3LE England

We prove a dichotomy theorem for the rank of propositional contradictions, uniformly generated from first-order sentences, in both the Lovasz-Schrijver (LS) and Sherali-Adams (SA) refutation systems. More precisely, we first show that the propositional translations of first-order formulae that are universally false, that is, fail in all finite and infinite models, have LS proofs whose rank is constant, independent of the size of the (finite) universe. In contrast to that, we prove that the propositional formulae that fail in all finite models, but hold in some infinite structure, require proofs whose SA rank grows polynomially with the size of the universe. Until now, this kind of so-called complexity gap theorem has been known for tree-like Resolution and, in somehow restricted forms, for the Resolution and Nullstellensatz systems. As far as we are aware, this is the first time the Sherali-Adams lift-and-project method has been considered as a propositional refutation system (since the conference version of this paper, SA has been considered as a refutation system in several further papers). An interesting feature of the SA system is that it simulates LS, the Lovasz-Schrijver refutation system without semi-definite cuts, in a rank-preserving fashion.

关键词： propositional proof complexity lift-and-project methods Lovasz-Schrijver proof system lower bounds complexity gap theorems

来源：评论

学校读者我要写书评

暂无评论

ON OPTIMAL HEURISTIC RANDOMIZED SEMIDECISION PROCEDURES, WITH APPLICATION TO proof complexity

ON OPTIMAL HEURISTIC RANDOMIZED SEMIDECISION PROCEDURES, WIT...

引用

27th International Symposium on Theoretical Aspects of Computer Science (STACS)

作者： Hirsch, Edward A. Itsykson, Dmitry Steklov Inst Math St Petersburg 27 Fontanka St Petersburg 191023 Russia

ISBN: (纸本)9783939897163

The existence of a (p-) optimal propositional proof system is a major open question in (proof) complexity;many people conjecture that such systems do not exist. Krajicek and Pudlak [KP89] show that this question is equivalent to the existence of an algorithm that is optimal(1) on all propositional tautologies. Monroe [Mon09] recently gave a conjecture implying that such algorithm does not exist. We show that in the presence of errors such optimal algorithms do exist. The concept is motivated by the notion of heuristic algorithms. Namely, we allow the algorithm to claim a small number of false "theorems" (according to any polynomial-time samplable distribution on non-tautologies) and err with bounded probability on other inputs. Our result can also be viewed as the existence of an optimal proof system in a class of proof systems obtained by generalizing automatizable proof systems.

关键词： propositional proof complexity optimal algorithm

来源：评论

学校读者我要写书评

暂无评论

On the complexity of the Sperner Lemma

On the complexity of the Sperner Lemma

引用

2nd Conference on Computability in Europe (CiE 2006)

作者： Dantchev, Stefan Univ Durham Dept Comp Sci Sci Labs Durham DH1 3LE England

We present a reduction from the Pigeon-Hole Principle to the classical Sperner Lemma. The reduction is used 1. to show that the Sperner Lemma does not have a short constant-depth Frege proof, and 2. to prove lower bou... 详细信息

ISBN: (纸本)3540354662

关键词： propositional proof complexity constant-depth frege search problems query complexity Sperner Lemma pigeon-hole principle

来源：评论

学校读者我要写书评

暂无评论

Rank complexity Gap for Lovasz-Schrijver and Sherali-Adams proof Systems 07

Rank Complexity Gap for Lovasz-Schrijver and Sherali-Adams P...

引用

39th Annual ACM Symposium on Theory of Computing

作者： Dantchev, Stefan Univ Durham Dept Comp Sci Durham DH1 3LE England

ISBN: (纸本)9781595936318

We prove a dichotomy theorem for the rank of the uniformly generated (i.e. expressible in First-Order (170) Logic) propositional tautologies in both the Lovdsz-Schrijver (LS) and Sherali-Adams (SA) proof systems. More precisely, we first show that the propositional translations of FO formulae that are universally trite, i.e. hold in all finite and infinite models, have LS proofs whose rank is constant, independently from the size of the (finite) universe. In contrast to that, we prove that the propositional formulae that hold in all finite models but fail in some infinite structure require proofs whose SA rank grows poly-logarithmically with the size of the universe. Up to now, this kind of so-called "complexity Gap" theorems have been known for Tree-like Resolution and, in some-how restricted forms, for the Resolution and Nullstellensatz proof systems. As far as we are aware, this is the first time the Sherali-Adams lift-and-project method has been considered as a propositional proof system. An interesting feature of the SA proof system is that it is static and rank-preserving simulates LS, the Lovisz-Schrijver proof system without semidefinite cuts.

关键词： propositional proof complexity Lift and Project Methods Lovasz-Schrijver proof System Lower Bounds complexity Gap Theorems

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：