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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

On proof complexity of Resolution over Polynomial Calculus

引用

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC 2022年第3期23卷 16-16页

作者： Khaniki, Erfan Charles Univ Prague Zitna 25 Prague 11567 Czech Republic Czech Acad Sci Zitna 25 Prague 11567 Czech Republic

The proof system Res(PCd, (R)) is a natural extension of the Resolution proof system that instead of disjunctions of literals operates with disjunctions of degree d multivariate polynomials over a ring R with Boolean variables. Proving super-polynomial lower bounds for the size of Res( PC1, (R))-refutations of Conjunctive normal forms (CNFs) is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for Res( PC1,(F)) when F is a finite field, such as F-2. In this article, we investigate Res(PCd, (R)) and tree-like Res(PCd, (R)) and prove size-width relations for them when R is a finite ring. As an application, we prove new lower bounds and reprove some known lower bounds for every finite field F as follows: (1) We prove almost quadratic lower bounds for Res(PCd, F)-refutations for every fixed d. The new lower bounds are for the following CNFs: (a) Mod q Tseitin formulas (char (F) not equal q) and Flow formulas, (b) Random k-CNFs with linearly many clauses. (2) We also prove super-polynomial (more than nk for any fixed k) and also exponential (2(n epsilon) for an epsilon > 0) lower bounds for tree-like Res(PCd, F)-refutations based on how big d is with respect to n for the following CNFs: (a) Mod q Tseitin formulas (char (F) not equal q) and Flow formulas, (b) Random k-CNFs of suitable densities, (c) Pigeonhole principle and Counting mod q principle. The lower bounds for the dag-like systems are the first nontrivial lower bounds for these systems, including the case d = 1. The lower bounds for the tree-like systems were known for the case d = 1 (except for the Counting mod q principle, in which lower bounds for the case d > 1 were known too). Our lower bounds extend those results to the case where d > 1 and also give new proofs for the case d = 1.

关键词： Resolution resolution over linear equations Polynomial Calculus size-width relations modular counting lower bounds propositional pigeonhole principle Tseitin formulas propositional proof complexity

来源：评论

学校读者我要写书评

暂无评论

Knowledge Compilation Languages as proof Systems 1

引用

22nd International Conference on Theory and Applications of Satisfiability Testing (SAT)

作者： Capelli, Florent Univ Lille INRIA UMR 9189 CRIStAL Ctr Rech Informat Signal & Automat Lille F-59000 Lille France

ISBN: (数字)9783030242589

ISBN: (纸本)9783030242589;9783030242572

In this paper, we study proof systems in the sense of Cook-Reckhow for problems that are higher in the Polynomial Hierarchy than coNP, in particular, #SAT and maxSAT. We start by explaining how the notion of Cook-Reckhow proof systems can be apply to these problems and show how one can twist existing languages in knowledge compilation such as decision DNNF so that they can be seen as proof systems for problems such as #SAT and maxSAT.

关键词： Knowledge compilation propositional proof complexity propositional Model Counting maxSAT

来源：评论

学校读者我要写书评

暂无评论

Rank lower bounds for the sherali-adams operator

引用

3rd Conference on Computability in Europe (CiE 2007)

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

ISBN: (纸本)9783540730002

We consider the Sherali-Adams (SA) operator as a proof system for integer linear programming and prove linear lower bounds on the SA rank required to prove both the pigeon hole and least number principles. We also define the size of a SA proof and show that that while the pigeon hole principle requires linear rank, it only requires at most polynomial size.

关键词： propositional proof complexity lift and project proof systems rank lower bounds sherali-adams relaxation

来源：评论

学校读者我要写书评

暂无评论

Poly-logarithmic Frege Depth Lower Bounds via an Expander Switching Lemma 16

Poly-logarithmic Frege Depth Lower Bounds via an Expander Sw...

引用

48th Annual ACM SIGACT Symposium on Theory of Computing (STOC)

作者： Pitassi, Toniann Rossman, Benjamin Servedio, Rocco A. Tan, Li-Yang Univ Toronto Toronto ON Canada Natl Inst Informat Tokyo Japan Columbia Univ New York NY USA Toyota Technol Inst Chicago IL USA Simons Inst Berkeley CA USA

ISBN: (纸本)9781450341325

We show that any polynomial-size Frege refutation of a certain linear-size unsatisfiable 3-CNF formula over n variables must have depth Omega(root log n). This is an exponential improvement over the previous best results (Pitassi et al. 1993, Krajicek et al. 1995, Ben-Sasson 2002) which give Omega(log log n) lower bounds. The 3-CNF formulas which we use to establish this result are Tseitin contradictions on 3-regular expander graphs. In more detail, our main result is a proof that for every d, any depth-d Frege refutation of the Tseitin contradiction over these n-node graphs must have size n(Omega((log n)/d2)). A key ingredient of our approach is a new switching lemma for a carefully designed random restriction process over these expanders. These random restrictions reduce a Tseitin instance on a 3-regular n-node expander to a Tseitin instance on a random subgraph which is a topological embedding of a 3-regular n'-node expander, for some n' which is not too much less than n. Our result involves Omega (root log n) iterative applications of this type of random restriction.

关键词： propositional proof complexity Frege proof system small-depth circuits switching lemma random projections

来源：评论

学校读者我要写书评

暂无评论

An Exponential Lower Bound for proofs in Focused Calculi 26th

An Exponential Lower Bound for Proofs in Focused Calculi

引用

26th Workshop on Logic, Language, Information, and Computation (WoLLIC)

作者： Jalali, Raheleh Czech Acad Sci Inst Math Prague Czech Republic Charles Univ Prague Fac Math & Phys Prague Czech Republic

ISBN: (纸本)9783662595336;9783662595329

In [7], Iemhoff introduced a special form of sequent-style rules and axioms, which she called focused, and studied the relationship between the focused proof systems, the systems only consisting of this kind of rules and axioms, and the uniform interpolation of the logic that the system captures. Subsequently, as a negative consequence of this relationship, she excludes almost all super-intuitionistic logics from having these focused proof systems. In this paper, we will provide a complexity theoretic analogue of her negative result to show that even in the cases that these systems exist, their proof-length would computationally explode. More precisely, we will first introduce two natural subclasses of focused rules, called PPF and MPF rules. Then, we will introduce some CPC-valid (IPC-valid) sequents with polynomially short tree-like proofs in the usual Hilbert-style proof system for classical logic, or equivalently LK + Cut, that have exponentially long proofs in the systems only consisting of PPF (MPF) rules.

关键词： Focused calculi propositional proof complexity Feasible interpolation Super-intuitionistic logics

来源：评论

学校读者我要写书评

暂无评论

SNARGs under LWE via propositional proofs 2024

SNARGs under LWE via Propositional Proofs

引用

56th Annual ACM Symposium on Theory of Computing (STOC)

作者： Jin, Zhengzhong Kalai, Yael Lombardi, Alex Vaikuntanathan, Vinod Northeastern Univ Boston MA 02115 USA MIT Cambridge MA USA Microsoft Res Cambridge MA USA Princeton Univ Princeton NJ USA

ISBN: (纸本)9798400703836

We construct a succinct non-interactive argument (SNARG) system for every NP language L that has a propositional proof of non-membership, i.e. of x is not an element of L. The soundness of our SNARG system relies on the hardness of the learning with errors (LWE) problem. The common reference string (CRS) in our construction grows with the space required to verify the propositional proof, and the size of the proof grows poly-logarithmically in the length of the propositional proof. Unlike most of the literature on SNARGs, our result implies SNARGs for languages L with proof length shorter than logarithmic in the deterministic time complexity of L. Our SNARG improves over prior SNARGs for such "hard" NP languages (Sahai and Waters, STOC 2014, Jain and Jin, FOCS 2022) in several ways: 1) For languages with polynomial-length propositional proofs of non-membership, our SNARGs are based on a single, polynomialtime falsifiable assumption, namely LWE. 2) Our construction handles super-polynomial length propositional proofs, as long as they have bounded space, under the subex-ponential LWE assumption. 3) Our SNARGs have a transparent setup, meaning that no private randomness is required to generate the CRS. Moreover, our approach departs dramatically from these prior works: we show how to design SNARGs for hard languages without publishing a program (in the CRS) that has the power to verify NP witnesses. The key new idea in our construction is what we call a "locally unsatisable extension" of the NP verication circuit {C-x}(x). We say that an NP verifier has a locally unsatisfiable extension if for every x is not an element of L, there exists an extension E-x of C-x that is not even locally satisfiable in the sense of a local assignment generator [Paneth-Rothblum, TCC 2017]. Crucially, we allow E-x to be depend arbitrarily on G rather than being efficiently constructible. In this work, we show - via a "hash-and-BARG" for a hidden, encrypted computation - how to build SNARGs

关键词： SNARGs Delegation of Computation propositional proof complexity

来源：评论

学校读者我要写书评

暂无评论

Improved lower bounds for tree-like resolution over linear inequalities

引用

10th International Conference on Theory and Applications of Satisfiability Testing

作者： Kojevnikov, Arist VA Steklov Math Inst St Petersburg Dept 27 Fontanka St Petersburg 191023 Russia

ISBN: (纸本)9783540727873

We continue a study initiated by Krajicek of a Resolution-like proof system working with clauses of linear inequalities, R(CP). For all proof systems of this kind Krajicek proved in [1] an exponential lower bound of the form: exp(n(Omega(1)))/M-O(W log2n), where M is the maximal absolute value of coefficients in a given proof and W is the maximal clause width. In this paper we improve this lower bound. For tree-like R(CP)-like proof systems we remove a dependence on the maximal absolute value of coefficients M, hence, we give the answer to an open question from [2]. proof follows from an upper bound on the real communication complexity of a polyhedra.

关键词： propositional proof complexity integer programming cutting planes

来源：评论

学校读者我要写书评

暂无评论

Resolution width and Cutting Plane rank are incomparable

引用

33rd International Symposium on Mathematical Foundations of Computer Science

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

ISBN: (纸本)9783540852377

We demonstrate that the Cutting Plane (CP) rank of a polytope defined by a system of inequalities derived from a set of unsatisfiable clauses can be arbitrarily larger than the Resolution width of the clauses, thus demonstrating the two measures are incomparable. More specifically, we show there exists an infinite family of unsatisfiable clauses defined over n is an element of N, which have constant Resolution width, but, yield polytopes which have CP rank Omega(log(2) n).

关键词： propositional proof complexity Cutting Plane proofs rank lower bounds Resolution width

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：