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

On the automatizability of resolution and related propositional proof systems

INFORMATION AND COMPUTATION 2004年第2期189卷 182-201页

作者： Atserias, A Bonet, ML Univ Politecn Cataluna Dept Llenguatges & Sistemes Informat Barcelona Spain

A propositional proof system is automatizable if there is an algorithm that, given a tautology, produces a proof in time polynomial in the size of its smallest proof. This notion can be weakened if we allow the algorithm to produce a proof in a stronger system within the same time bound. This new notion is called weak antomatizability. Among other characterizations, we prove that a system is weakly automatizable exactly when a weak form of the satisfiability problem is solvable in polynomial time. After studying the robustness of the definition, we prove the equivalence between: (i). Resolution is weakly automatizable, (ii) Res(k) is weakly automatizable, and (iii) Res(k) has feasible interpolation, when k > 1. In order to prove this result, we show that Res(2) has polynomial-size proofs of the reflection principle of Resolution, which is a version of consistency. We also show that Res(k), for every k > 1, proves its consistency in polynomial size, while Resolution does not. In fact, we show that Resolution proofs of its own consistency require almost exponential size. This gives a better lower bound for the monotone interpolation of Res(2) and a separation from Resolutionas a byproduct. Our techniques also give us a way to obtain a large class of examples that have small Resolution refutations but require relatively large width. This answers a question of Alekhnovich and Razborov related to whether Resolution is automatizable in quasipolynomial-time. (C) 2003 Elsevier Inc. All rights reserved.

关键词： propositional proof complexity feasible interpolation automatizability reflection principles resolution Res(2)

来源：评论

学校读者我要写书评

暂无评论

Some Subsystems of Constant-Depth Frege with Parity

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2018年第4期19卷 1–34页

作者： Garlik, Michal Kolodziejczyk, Leszek Aleksander Univ Warsaw Inst Math Banacha 2 PL-02097 Warsaw Poland Univ Politecn Cataluna C Jordi Girona 1-3 ES-08034 Barcelona Spain

We consider three relatively strong families of subsystems of AC(0)[2]-Frege proof systems, i.e., propositional proof systems using constant-depth formulas with an additional parity connective, for which exponential lower bounds on proof size are known. In order of increasing strength, the subsystems are (i) constant-depth proof systems with parity axioms and the (ii) treelike and (iii) daglike versions of systems introduced by Krajicek which we call PKdc (circle plus). In a PKdc (circle plus)-proof, lines are disjunctions (cedents) in which all disjuncts have depth at most d, parities can only appear as the outermost connectives of disjuncts, and all but c disjuncts contain no parity connective at all. We prove that treelike PKO(1)O(1) (circle plus) is quasipolynomially but not polynomially equivalent to constant-depth systems with parity axioms. We also verify that the technique for separating parity axioms from parity connectives due to Impagliazzo and Segerlind can be adapted to give a superpolynomial separation between daglike PKO(1)O(1) (circle plus) and AC(0)[2]-Frege;the technique is inherently unable to prove superquasipolynomial separations. We also study proof systems related to the system Res-Lin introduced by Itsykson and Sokolov. We prove that an extension of treelike Res-Lin is polynomially simulated by a system related to daglike PKO(1)O(1) (circle plus), and obtain an exponential lower bound for this system.

关键词： Constant-depth Frege modular counting counting axioms propositional proof complexity

来源：评论

学校读者我要写书评

暂无评论

A switching lemma for small restrictions and lower bounds for k-DNF resolution

引用

SIAM JOURNAL ON COMPUTING 2004年第5期33卷 1171-1200页

作者： Segerlind, N Buss, S Impagliazzo, R Inst Adv Study Sch Math Princeton NJ 08540 USA Univ Calif San Diego Dept Math La Jolla CA 92092 USA Univ Calif San Diego Dept Comp Sci La Jolla CA 92092 USA

We prove a new switching lemma that works for restrictions that set only a small fraction of the variables and is applicable to formulas in disjunctive normal form (DNFs) with small terms. We use this to prove lower bounds for the Res(k) propositional proof system, an extension of resolution which works with k-DNFs instead of clauses. We also obtain an exponential separation between depth d circuits of bottom fan-in k and depth d circuits of bottom fan-in k+1. Our results for Res(k) are as follows: 1. The 2n to n weak pigeonhole principle requires exponential size to refute in Res(k) for krootlog n/log log n. 2. For each constant k, there exists a constant w>k so that random w-CNFs require exponential size to refute in Res(k). 3. For each constant k, there are sets of clauses which have polynomial size Res(k+1) refutations but which require exponential size Res(k) refutations.

关键词： propositional proof complexity Boolean circuit complexity switching lemmas lower bounds k-DNFs resolution Res(k) circuit bottom fan-in random restriction Sipser functions weak pigeonhole principles random CNFs

来源：评论

学校读者我要写书评

暂无评论

The Ordering Principle in a Fragment of Approximate Counting

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2014年第4期15卷 1-11页

作者： Atserias, Albert Thapen, Neil Univ Politecn Cataluna Dept Llenguatges & Sistemes Informat ES-08034 Barcelona Spain Acad Sci Czech Republic Inst Math CR-11567 Prague 1 Czech Republic

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over T-2(1). This answers an open question raised in Buss et al. [2012] and completes their program to compare the strength of Jerabek's bounded arithmetic theory for approximate counting with weakened versions of it.

关键词： Theory Algorithms Computational complexity bounded arithmetic propositional proof complexity polynomial local search

来源：评论

学校读者我要写书评

暂无评论

Exponential separation between Res (k) and Res (k+1) for k ≤ ε log n

引用

INFORMATION PROCESSING LETTERS 2005年第4期93卷 185-190页

作者： Segerlind, N Inst Adv Study Sch Math Princeton NJ 08540 USA

Res(k) is a propositional proof system that extends resolution by working with k-DNFs instead of clauses. We show that there exist constants beta, gamma > 0 so that if k is a function from positive integers to positive integers so that for all n, k(n) less than or equal to beta log n, then for each n, there exists a set of clauses C-n of size n(O(1)) that has Res(k(n) + 1) refutations of size n(O(1)), yet every Res(k(n)) refutation of C-n has size at least 2(ngamma). (C) 2004 Elsevier B.V. All rights reserved.

关键词： propositional proof complexity lower bounds k-DNFs resolution Res(k) switching lemmas random restrictions theory of computation computational complexity

来源：评论

学校读者我要写书评

暂无评论

Bounded-depth Frege lower bounds for weaker pigeonhole principles

引用

SIAM JOURNAL ON COMPUTING 2004年第2期34卷 261-276页

作者： Buresh-Oppenheim, J Beame, P Pitassi, T Raz, R Sabharwal, A Univ Toronto Dept Comp Sci Toronto ON M5S 3G4 Canada Univ Washington Seattle WA 98195 USA Weizmann Inst Sci Fac Math & Comp Sci IL-76100 Rehovot Israel

We prove a quasi-polynomial lower bound on the size of bounded-depth Frege proofs of the pigeonhole principle PHPnm where m = (1 + 1/ polylog n)n. This lower bound qualitatively matches the known quasi-polynomial-size bounded-depth Frege proofs for these principles. Our technique, which uses a switching lemma argument like other lower bounds for bounded-depth Frege proofs, is novel in that the tautology to which this switching lemma is applied remains random throughout the argument.

关键词： propositional proof complexity pigeonhole principle

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Constant-depth Frege systems with counting axioms polynomially simulate Nullstellensatz refutations

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2006年第2期7卷 199-218页

作者： Impagliazzo, Russell Segerlind, Nathan Univ Calif San Diego Dept Comp Sci San Diego CA 92103 USA Inst Adv Study Sch Math Princeton NJ 08540 USA

We show that constant-depth Frege systems with counting axioms modulo m polynomially simulate Nullstellensatz refutations modulo m. Central to this is a new definition of reducibility from propositional formulas to systems of polynomials. Using our definition of reducibility, most previously studied propositional formulas reduce to their polynomial translations. When combined with a previous result of the authors, this establishes the first size separation between Nullstellensatz and polynomial calculus refutations. We also obtain new upper bounds on refutation sizes for certain CNFs in constant-depth Frege with counting axioms systems.

关键词： theory modular counting axioms Nullstellensatz refutations propositional proof complexity

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

SIZE-SPACE TRADEOFFS FOR RESOLUTION

引用

SIAM JOURNAL ON COMPUTING 2009年第6期38卷 2511-2525页

作者： Ben-Sasson, Eli Technion Israel Inst Technol Dept Comp Sci IL-32000 Haifa Israel

We investigate tradeoffs of various basic complexity measures such as size, space, and width. We show examples of formulas that have optimal proofs with respect to any one of these parameters, but optimizing one parameter must cost an increase in the other. These results have implications to the efficiency (or rather, inefficiency) of some commonly used SAT solving heuristics. Our proof relies on a novel connection of the variable space of a proof to the black-white pebbling measure of an underlying graph.

关键词： propositional proof complexity resolution proof length automated theorem provers

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：