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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

A LIMITATION ON THE KPT INTERPOLATION

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2020年第3期16卷 1-95页

作者： Krajicek, Jan Charles Univ Prague MFF Sokolovska 83 Prague 18675 Czech Republic

We prove a limitation on a variant of the KPT theorem proposed for propositional proof systems by Pich and Santhanam [7], for all proof systems that prove the disjointness of two NP sets that are hard to distinguish.

关键词： propositional proof complexity interpolation KPT theorem

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：