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

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 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

来源：评论

学校读者我要写书评

暂无评论

The limits of tractability in Resolution-based propositional proof systems

引用

ANNALS OF PURE AND APPLIED LOGIC 2012年第6期163卷 656-668页

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

We study classes of propositional contradictions based on the Least Number Principle (LNP) in the refutation system of Resolution and its generalisations with bounded conjunction, Res(k). We prove that any first-order sentence with no finite models that admits a Sigma(1) interpretation of the LNP, relativised to a set that is quantifier-free definable, generates a sequence of propositional contradictions that have polynomially-sized refutations in the system Res(k), for some k. When one considers the LNP with total order we demonstrate that a Pi(1) interpretation of this is sufficient to generate such a propositional sequence with polynomially-sized refutations in the system Res(k). On the other hand, we prove that a very simple first-order sentence that admits a Pi(1) interpretation of the LNP (with partial and not total order) requires exponentially-sized refutations in both Resolution and Res(k), for all constant k. (c) 2011 Elsevier B.V. All rights reserved.

关键词： propositional proof complexity Resolution with bounded conjunction Lower bounds

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

LOWER BOUNDS FOR K-DNF RESOLUTION ON RANDOM 3-CNFS

引用

COMPUTATIONAL complexity 2011年第4期20卷 597-614页

作者： Alekhnovich, Michael Inst Adv Study Princeton NJ 08540 USA

We prove exponential lower bounds on refutations of a random 3-CNF with linear number of clauses by k-DNF Resolution for k <= root log n/log log n. For this we design a specially tailored random restrictions that preserve the structure of the input random 3-CNF while mapping every k-DNF with large covering number to one with high probability. Next we make use of the switching lemma for small restrictions by Segerlind, Buss and Impagliazzo to prove the lower bound. This work improves the previously known lower bound for Res(2) system on random 3-CNFs by Atserias, Bonet and Esteban and the result of Segerlind, Buss, Impagliazzo stating that random O(k(2))-CNF do not possess short Res(k)refutations.

关键词： propositional proof complexity random CNFs

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Random Cnf's are Hard for the Polynomial Calculus

引用

COMPUTATIONAL complexity 2010年第4期19卷 501-519页

作者： Ben-Sasson, Eli Impagliazzo, Russell Technion Israel Inst Technol Dept Comp Sci IL-32000 Haifa Israel Inst Adv Study Sch Math Princeton NJ 08540 USA Univ Calif San Diego La Jolla CA 92093 USA

We prove linear lower bounds on the Polynomial Calculus (PC) refutation-degree of random CNF whenever the underlying field has characteristic greater than 2. Our proof follows by showing the PC refutation-degree of a unsatisfiable system of linear equations modulo 2 is equivalent to its Gaussian width, a concept defined by the late Mikhail Alekhnovich. The equivalence of refutation-degree and Gaussian width which is the main contribution of this paper, allows us to also simplify the refutation-degree lower bounds of Buss et al. (2001) and additionally prove non-trivial upper bounds on the resolution and PC complexity of refuting unsatisfiable systems of linear equations.

关键词： propositional proof complexity polynomial calculus Groebner basis random CNF formulae

来源：评论

学校读者我要写书评

暂无评论

complexity of propositional proofs Under a Promise

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2010年第3期11卷 18-18页

作者： Dershowitz, Nachum Tzameret, Iddo Tel Aviv Univ Sch Comp Sci IL-69978 Tel Aviv Israel Acad Sci Czech Republic Inst Math CZ-11567 Prague Czech Republic

We study-within the framework of propositional proof complexity-the problem of certifying un-satisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where many stands for an explicitly specified function Lambda in the number of variables n. To this end, we develop propositional proof systems under different measures of promises (i. e., different Lambda) as extensions of resolution. This is done by augmenting resolution with axioms that, roughly, can eliminate sets of truth assignments defined by Boolean circuits. We then investigate the complexity of such systems, obtaining an exponential separation in the average case between resolution under different size promises: (1) Resolution has polynomial-size refutations for all unsatisfiable 3CNF formulas when the promise is epsilon.2(n), for any constant 0 < epsilon < 1. (2) There are no subexponential size resolution refutations for random 3CNF formulas, when the promise is 2(delta n), for any constant 0 < delta < 1 (and the number of clauses is O(n(3/2-epsilon)), for 0 < epsilon < 1/2).

关键词： Theory Promise problems propositional proof complexity random 3CNF resolution

来源：评论

学校读者我要写书评

暂无评论

Tight rank lower bounds for the Sherali-Adams proof system

引用

THEORETICAL COMPUTER SCIENCE 2009年第21-23期410卷 2054-2063页

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

We consider a proof (more accurately, refutation) system based on the Sherali-Adams (SA) operator associated with integer linear programming. If F is a CNF contradiction that admits a Resolution refutation of width k and size s. then we prove that the SA rank of F is <= k and the SA size of F is <= (k + 1)s + 1. We establish that the SA rank of both the Pigeonhole Principle PHPn-1n and the Least Number Principle LNPn is n - 2. Since the SA refutation system rank-simulates the refutation system of Lovasz-Schrijver without semidefinite cuts (LS), we obtain as a corollary linear rank lower bounds for both of these principles in LS. (C) 2009 Published by Elsevier B.V.

关键词： propositional proof complexity Lift-and-project methods

来源：评论

学校读者我要写书评

暂无评论

On the Chvatal rank of the Pigeonhole Principle

引用

THEORETICAL COMPUTER SCIENCE 2009年第27-29期410卷 2774-2778页

作者： Rhodes, Mark Univ Durham Dept Comp Sci Durham DH1 3LE England

We demonstrate that the Cutting Plane (CP) rank, also known as the Chvatal rank, of the Pigeonhole Principle is Theta(log n). Our proof uses a novel technique which allows us to demonstrate rank lower bounds for fractional points with fewer restrictions than previous methods. We also demonstrate that the Pigeonhole Principle has a polynomially sized CP proof. (C) 2009 Elsevier B.V. All rights reserved.

关键词： Pigeonhole principle propositional proof complexity Chvatal rank Cutting planes

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：