17 Search Results for "Pudlák, Pavel"

Document
DOI: 10.4230/LIPIcs.CCC.2024.17
Local Enumeration and Majority Lower Bounds

Authors: Mohit Gurumukhani, Ramamohan Paturi, Pavel Pudlák, Michael Saks, and Navid Talebanfard

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
Depth-3 circuit lower bounds and k-SAT algorithms are intimately related; the state-of-the-art Σ^k_3-circuit lower bound (Or-And-Or circuits with bottom fan-in at most k) and the k-SAT algorithm of Paturi, Pudlák, Saks, and Zane (J. ACM'05) are based on the same combinatorial theorem regarding k-CNFs. In this paper we define a problem which reveals new interactions between the two, and suggests a concrete approach to significantly stronger circuit lower bounds and improved k-SAT algorithms. For a natural number k and a parameter t, we consider the Enum(k, t) problem defined as follows: given an n-variable k-CNF and an initial assignment α, output all satisfying assignments at Hamming distance t(n) of α, assuming that there are no satisfying assignments of Hamming distance less than t(n) of α. We observe that an upper bound b(n, k, t) on the complexity of Enum(k, t) simultaneously implies depth-3 circuit lower bounds and k-SAT algorithms: - Depth-3 circuits: Any Σ^k_3 circuit computing the Majority function has size at least binom(n,n/2)/b(n, k, n/2). - k-SAT: There exists an algorithm solving k-SAT in time O(∑_{t=1}^{n/2}b(n, k, t)). A simple construction shows that b(n, k, n/2) ≥ 2^{(1 - O(log(k)/k))n}. Thus, matching upper bounds for b(n, k, n/2) would imply a Σ^k_3-circuit lower bound of 2^Ω(log(k)n/k) and a k-SAT upper bound of 2^{(1 - Ω(log(k)/k))n}. The former yields an unrestricted depth-3 lower bound of 2^ω(√n) solving a long standing open problem, and the latter breaks the Super Strong Exponential Time Hypothesis. In this paper, we propose a randomized algorithm for Enum(k, t) and introduce new ideas to analyze it. We demonstrate the power of our ideas by considering the first non-trivial instance of the problem, i.e., Enum(3, n/2). We show that the expected running time of our algorithm is 1.598ⁿ, substantially improving on the trivial bound of 3^{n/2} ≃ 1.732ⁿ. This already improves Σ^3_3 lower bounds for Majority function to 1.251ⁿ. The previous bound was 1.154ⁿ which follows from the work of Håstad, Jukna, and Pudlák (Comput. Complex.'95). By restricting ourselves to monotone CNFs, Enum(k, t) immediately becomes a hypergraph Turán problem. Therefore our techniques might be of independent interest in extremal combinatorics.
Cite as

Mohit Gurumukhani, Ramamohan Paturi, Pavel Pudlák, Michael Saks, and Navid Talebanfard. Local Enumeration and Majority Lower Bounds. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 17:1-17:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gurumukhani_et_al:LIPIcs.CCC.2024.17,
  author =	{Gurumukhani, Mohit and Paturi, Ramamohan and Pudl\'{a}k, Pavel and Saks, Michael and Talebanfard, Navid},
  title =	{{Local Enumeration and Majority Lower Bounds}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{17:1--17:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.17},
  URN =		{urn:nbn:de:0030-drops-204136},
  doi =		{10.4230/LIPIcs.CCC.2024.17},
  annote =	{Keywords: Depth 3 circuits, k-CNF satisfiability, Circuit lower bounds, Majority function}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2024.12
From Proof Complexity to Circuit Complexity via Interactive Protocols

Authors: Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Folklore in complexity theory suspects that circuit lower bounds against NC¹ or P/poly, currently out of reach, are a necessary step towards proving strong proof complexity lower bounds for systems like Frege or Extended Frege. Establishing such a connection formally, however, is already daunting, as it would imply the breakthrough separation NEXP ⊈ P/poly, as recently observed by Pich and Santhanam [Pich and Santhanam, 2023]. We show such a connection conditionally for the Implicit Extended Frege proof system (iEF) introduced by Krajíček [Krajíček, 2004], capable of formalizing most of contemporary complexity theory. In particular, we show that if iEF proves efficiently the standard derandomization assumption that a concrete Boolean function is hard on average for subexponential-size circuits, then any superpolynomial lower bound on the length of iEF proofs implies #P ⊈ FP/poly (which would in turn imply, for example, PSPACE ⊈ P/poly). Our proof exploits the formalization inside iEF of the soundness of the sum-check protocol of Lund, Fortnow, Karloff, and Nisan [Lund et al., 1992]. This has consequences for the self-provability of circuit upper bounds in iEF. Interestingly, further improving our result seems to require progress in constructing interactive proof systems with more efficient provers.
Cite as

Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arteche_et_al:LIPIcs.ICALP.2024.12,
  author =	{Arteche, Noel and Khaniki, Erfan and Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{From Proof Complexity to Circuit Complexity via Interactive Protocols}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{12:1--12:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.12},
  URN =		{urn:nbn:de:0030-drops-201557},
  doi =		{10.4230/LIPIcs.ICALP.2024.12},
  annote =	{Keywords: proof complexity, circuit complexity, interactive protocols}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2024.63
TFNP Intersections Through the Lens of Feasible Disjunction

Authors: Pavel Hubáček, Erfan Khaniki, and Neil Thapen

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
The complexity class CLS was introduced by Daskalakis and Papadimitriou (SODA 2010) to capture the computational complexity of important TFNP problems solvable by local search over continuous domains and, thus, lying in both PLS and PPAD. It was later shown that, e.g., the problem of computing fixed points guaranteed by Banach’s fixed point theorem is CLS-complete by Daskalakis et al. (STOC 2018). Recently, Fearnley et al. (J. ACM 2023) disproved the plausible conjecture of Daskalakis and Papadimitriou that CLS is a proper subclass of PLS∩PPAD by proving that CLS = PLS∩PPAD. To study the possibility of other collapses in TFNP, we connect classes formed as the intersection of existing subclasses of TFNP with the phenomenon of feasible disjunction in propositional proof complexity; where a proof system has the feasible disjunction property if, whenever a disjunction F ∨ G has a small proof, and F and G have no variables in common, then either F or G has a small proof. Based on some known and some new results about feasible disjunction, we separate the classes formed by intersecting the classical subclasses PLS, PPA, PPAD, PPADS, PPP and CLS. We also give the first examples of proof systems which have the feasible interpolation property, but not the feasible disjunction property.
Cite as

Pavel Hubáček, Erfan Khaniki, and Neil Thapen. TFNP Intersections Through the Lens of Feasible Disjunction. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 63:1-63:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hubacek_et_al:LIPIcs.ITCS.2024.63,
  author =	{Hub\'{a}\v{c}ek, Pavel and Khaniki, Erfan and Thapen, Neil},
  title =	{{TFNP Intersections Through the Lens of Feasible Disjunction}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{63:1--63:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.63},
  URN =		{urn:nbn:de:0030-drops-195917},
  doi =		{10.4230/LIPIcs.ITCS.2024.63},
  annote =	{Keywords: TFNP, feasible disjunction, proof complexity, TFNP intersection classes}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.4
Linear Branching Programs and Directional Affine Extractors

Authors: Svyatoslav Gryaznov, Pavel Pudlák, and Navid Talebanfard

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
A natural model of read-once linear branching programs is a branching program where queries are 𝔽₂ linear forms, and along each path, the queries are linearly independent. We consider two restrictions of this model, which we call weakly and strongly read-once, both generalizing standard read-once branching programs and parity decision trees. Our main results are as follows. - Average-case complexity. We define a pseudo-random class of functions which we call directional affine extractors, and show that these functions are hard on average for the strongly read-once model. We then present an explicit construction of such function with good parameters. This strengthens the result of Cohen and Shinkar (ITCS'16) who gave such average-case hardness for parity decision trees. Directional affine extractors are stronger than the more familiar class of affine extractors. Given the significance of these functions, we expect that our new class of functions might be of independent interest. - Proof complexity. We also consider the proof system Res[⊕], which is an extension of resolution with linear queries, and define the regular variant of Res[⊕]. A refutation of a CNF in this proof system naturally defines a linear branching program solving the corresponding search problem. If a refutation is regular, we prove that the resulting program is read-once. Conversely, we show that a weakly read-once linear BP solving the search problem can be converted to a regular Res[⊕] refutation with constant blow up, where the regularity condition comes from the definition of weakly read-once BPs, thus obtaining the equivalence between these proof systems.
Cite as

Svyatoslav Gryaznov, Pavel Pudlák, and Navid Talebanfard. Linear Branching Programs and Directional Affine Extractors. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 4:1-4:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gryaznov_et_al:LIPIcs.CCC.2022.4,
  author =	{Gryaznov, Svyatoslav and Pudl\'{a}k, Pavel and Talebanfard, Navid},
  title =	{{Linear Branching Programs and Directional Affine Extractors}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{4:1--4:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.4},
  URN =		{urn:nbn:de:0030-drops-165664},
  doi =		{10.4230/LIPIcs.CCC.2022.4},
  annote =	{Keywords: Boolean Functions, Average-Case Lower Bounds, AC0\lbrack2\rbrack, Affine Dispersers, Affine Extractors}
}
Document
DOI: 10.4230/LIPIcs.CCC.2022.17
Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds

Authors: Erfan Khaniki

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
A map g:{0,1}ⁿ → {0,1}^m (m > n) is a hard proof complexity generator for a proof system P iff for every string b ∈ {0,1}^m ⧵ Rng(g), formula τ_b(g) naturally expressing b ∉ Rng(g) requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is Nisan-Wigderson generator. Razborov [A. A. {Razborov}, 2015] conjectured that if A is a suitable matrix and f is a NP∩CoNP function hard-on-average for 𝖯/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege. In this paper, we prove a form of Razborov’s conjecture for AC⁰-Frege. We show that for any symmetric NP∩CoNP function f that is exponentially hard for depth two AC⁰ circuits, NW_{f,A} is a hard proof complexity generator for AC⁰-Frege in a natural setting. As direct applications of this theorem, we show that: 1) For any f with the specified properties, τ_b(NW_{f,A}) (for a natural formalization) based on a random b and a random matrix A with probability 1-o(1) is a tautology and requires superpolynomial (or even exponential) AC⁰-Frege proofs. 2) Certain formalizations of the principle f_n ∉ (NP∩CoNP)/poly requires superpolynomial AC⁰-Frege proofs. These applications relate to two questions that were asked by Krajíček [J. {Krajíček}, 2019].
Cite as

Erfan Khaniki. Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{khaniki:LIPIcs.CCC.2022.17,
  author =	{Khaniki, Erfan},
  title =	{{Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{17:1--17:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.17},
  URN =		{urn:nbn:de:0030-drops-165799},
  doi =		{10.4230/LIPIcs.CCC.2022.17},
  annote =	{Keywords: Proof complexity, Bounded arithmetic, Bounded depth Frege, Nisan-Wigderson generators, Meta-complexity, Lower bounds}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.35
Equivalence of Systematic Linear Data Structures and Matrix Rigidity

Authors: Sivaramakrishnan Natarajan Ramamoorthy and Cyrus Rashtchian

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
Recently, Dvir, Golovnev, and Weinstein have shown that sufficiently strong lower bounds for linear data structures would imply new bounds for rigid matrices. However, their result utilizes an algorithm that requires an NP oracle, and hence, the rigid matrices are not explicit. In this work, we derive an equivalence between rigidity and the systematic linear model of data structures. For the n-dimensional inner product problem with m queries, we prove that lower bounds on the query time imply rigidity lower bounds for the query set itself. In particular, an explicit lower bound of ω(n/r log m) for r redundant storage bits would yield better rigidity parameters than the best bounds due to Alon, Panigrahy, and Yekhanin. We also prove a converse result, showing that rigid matrices directly correspond to hard query sets for the systematic linear model. As an application, we prove that the set of vectors obtained from rank one binary matrices is rigid with parameters matching the known results for explicit sets. This implies that the vector-matrix-vector problem requires query time Ω(n^(3/2)/r) for redundancy r ≥ √n in the systematic linear model, improving a result of Chakraborty, Kamma, and Larsen. Finally, we prove a cell probe lower bound for the vector-matrix-vector problem in the high error regime, improving a result of Chattopadhyay, Koucký, Loff, and Mukhopadhyay.
Cite as

Sivaramakrishnan Natarajan Ramamoorthy and Cyrus Rashtchian. Equivalence of Systematic Linear Data Structures and Matrix Rigidity. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 35:1-35:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{natarajanramamoorthy_et_al:LIPIcs.ITCS.2020.35,
  author =	{Natarajan Ramamoorthy, Sivaramakrishnan and Rashtchian, Cyrus},
  title =	{{Equivalence of Systematic Linear Data Structures and Matrix Rigidity}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{35:1--35:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.35},
  URN =		{urn:nbn:de:0030-drops-117204},
  doi =		{10.4230/LIPIcs.ITCS.2020.35},
  annote =	{Keywords: matrix rigidity, systematic linear data structures, cell probe model, communication complexity}
}
Document
DOI: 10.4230/DagRep.8.1.124
Proof Complexity (Dagstuhl Seminar 18051)

Authors: Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam

Published in: Dagstuhl Reports, Volume 8, Issue 1 (2018)

Abstract
The study of proof complexity was initiated in [Cook and Reckhow 1979] as a way to attack the P vs.NP problem, and in the ensuing decades many powerful techniques have been discovered for analyzing different proof systems. Proof complexity also gives a way of studying subsystems of Peano Arithmetic where the power of mathematical reasoning is restricted, and to quantify how complex different mathematical theorems are measured in terms of the strength of the methods of reasoning required to establish their validity. Moreover, it allows to analyse the power and limitations of satisfiability algorithms (SAT solvers) used in industrial applications with formulas containing up to millions of variables. During the last 10--15 years the area of proof complexity has seen a revival with many exciting results, and new connections have also been revealed with other areas such as, e.g., cryptography, algebraic complexity theory, communication complexity, and combinatorial optimization. While many longstanding open problems from the 1980s and 1990s still remain unsolved, recent progress gives hope that the area may be ripe for decisive breakthroughs. This workshop, gathering researchers from different strands of the proof complexity community, gave opportunities to take stock of where we stand and discuss the way ahead.
Cite as

Albert Atserias, Jakob Nordström, Pavel Pudlák, and Rahul Santhanam. Proof Complexity (Dagstuhl Seminar 18051). In Dagstuhl Reports, Volume 8, Issue 1, pp. 124-157, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{atserias_et_al:DagRep.8.1.124,
  author =	{Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul},
  title =	{{Proof Complexity (Dagstuhl Seminar 18051)}},
  pages =	{124--157},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{8},
  number =	{1},
  editor =	{Atserias, Albert and Nordstr\"{o}m, Jakob and Pudl\'{a}k, Pavel and Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.8.1.124},
  URN =		{urn:nbn:de:0030-drops-92864},
  doi =		{10.4230/DagRep.8.1.124},
  annote =	{Keywords: bounded arithmetic, computational complexity, logic, proof complexity, satisfiability algorithms}
}
Document
DOI: 10.4230/LIPIcs.CCC.2017.1
Random Resolution Refutations

Authors: Pavel Pudlák and Neil Thapen

Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)

Abstract
We study the random resolution refutation system definedin [Buss et al. 2014]. This attempts to capture the notion of a resolution refutation that may make mistakes but is correct most of the time. By proving the equivalence of several different definitions, we show that this concept is robust. On the other hand, if P does not equal NP, then random resolution cannot be polynomially simulated by any proof system in which correctness of proofs is checkable in polynomial time. We prove several upper and lower bounds on the width and size of random resolution refutations of explicit and random unsatisfiable CNF formulas. Our main result is a separation between polylogarithmic width random resolution and quasipolynomial size resolution, which solves the problem stated in [Buss et al. 2014]. We also prove exponential size lower bounds on random resolution refutations of the pigeonhole principle CNFs, and of a family of CNFs which have polynomial size refutations in constant depth Frege.
Cite as

Pavel Pudlák and Neil Thapen. Random Resolution Refutations. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 1:1-1:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{pudlak_et_al:LIPIcs.CCC.2017.1,
  author =	{Pudl\'{a}k, Pavel and Thapen, Neil},
  title =	{{Random Resolution Refutations}},
  booktitle =	{32nd Computational Complexity Conference (CCC 2017)},
  pages =	{1:1--1:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-040-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{79},
  editor =	{O'Donnell, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.1},
  URN =		{urn:nbn:de:0030-drops-75235},
  doi =		{10.4230/LIPIcs.CCC.2017.1},
  annote =	{Keywords: proof complexity, random, resolution}
}
Document
DOI: 10.4230/LIPIcs.CCC.2017.3
Representations of Monotone Boolean Functions by Linear Programs

Authors: Mateus de Oliveira Oliveira and Pavel Pudlák

Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)

Abstract
We introduce the notion of monotone linear-programming circuits (MLP circuits), a model of computation for partial Boolean functions. Using this model, we prove the following results. 1. MLP circuits are superpolynomially stronger than monotone Boolean circuits. 2. MLP circuits are exponentially stronger than monotone span programs. 3. MLP circuits can be used to provide monotone feasibility interpolation theorems for Lovasz-Schrijver proof systems, and for mixed Lovasz-Schrijver proof systems. 4. The Lovasz-Schrijver proof system cannot be polynomially simulated by the cutting planes proof system. This is the first result showing a separation between these two proof systems. Finally, we discuss connections between the problem of proving lower bounds on the size of MLPs and the problem of proving lower bounds on extended formulations of polytopes.
Cite as

Mateus de Oliveira Oliveira and Pavel Pudlák. Representations of Monotone Boolean Functions by Linear Programs. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{deoliveiraoliveira_et_al:LIPIcs.CCC.2017.3,
  author =	{de Oliveira Oliveira, Mateus and Pudl\'{a}k, Pavel},
  title =	{{Representations of Monotone Boolean Functions by Linear Programs}},
  booktitle =	{32nd Computational Complexity Conference (CCC 2017)},
  pages =	{3:1--3:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-040-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{79},
  editor =	{O'Donnell, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.3},
  URN =		{urn:nbn:de:0030-drops-75200},
  doi =		{10.4230/LIPIcs.CCC.2017.3},
  annote =	{Keywords: Monotone Linear Programming Circuits, Lov\'{a}sz-Schrijver Proof System, Cutting-Planes Proof System, Feasible Interpolation, Lower Bounds}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.85
Tighter Hard Instances for PPSZ

Authors: Pavel Pudlák, Dominik Scheder, and Navid Talebanfard

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We construct uniquely satisfiable k-CNF formulas that are hard for the PPSZ algorithm, the currently best known algorithm solving k-SAT. This algorithm tries to generate a satisfying assignment by picking a random variable at a time and attempting to derive its value using some inference heuristic and otherwise assigning a random value. The "weak PPSZ" checks all subformulas of a given size to derive a value and the "strong PPSZ" runs resolution with width bounded by some given function. Firstly, we construct graph-instances on which "weak PPSZ" has savings of at most (2 + epsilon)/k; the saving of an algorithm on an input formula with n variables is the largest gamma such that the algorithm succeeds (i.e. finds a satisfying assignment) with probability at least 2^{- (1 - gamma) n}. Since PPSZ (both weak and strong) is known to have savings of at least (pi^2 + o(1))/6k, this is optimal up to the constant factor. In particular, for k=3, our upper bound is 2^{0.333... n}, which is fairly close to the lower bound 2^{0.386... n} of Hertli [SIAM J. Comput.'14]. We also construct instances based on linear systems over F_2 for which strong PPSZ has savings of at most O(log(k)/k). This is only a log(k) factor away from the optimal bound. Our constructions improve previous savings upper bound of O((log^2(k))/k) due to Chen et al. [SODA'13].
Cite as

Pavel Pudlák, Dominik Scheder, and Navid Talebanfard. Tighter Hard Instances for PPSZ. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 85:1-85:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{pudlak_et_al:LIPIcs.ICALP.2017.85,
  author =	{Pudl\'{a}k, Pavel and Scheder, Dominik and Talebanfard, Navid},
  title =	{{Tighter Hard Instances for PPSZ}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{85:1--85:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.85},
  URN =		{urn:nbn:de:0030-drops-74144},
  doi =		{10.4230/LIPIcs.ICALP.2017.85},
  annote =	{Keywords: k-SAT, Strong Exponential Time Hypothesis, PPSZ, Resolution}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.35
Semantic Versus Syntactic Cutting Planes

Authors: Yuval Filmus, Pavel Hrubeš, and Massimo Lauria

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
In this paper, we compare the strength of the semantic and syntactic version of the cutting planes proof system. First, we show that the lower bound technique of Pudlák applies also to semantic cutting planes: the proof system has feasible interpolation via monotone real circuits, which gives an exponential lower bound on lengths of semantic cutting planes refutations. Second, we show that semantic refutations are stronger than syntactic ones. In particular, we give a formula for which any refutation in syntactic cutting planes requires exponential length, while there is a polynomial length refutation in semantic cutting planes. In other words, syntactic cutting planes does not p-simulate semantic cutting planes. We also give two incompatible integer inequalities which require exponential length refutation in syntactic cutting planes. Finally, we pose the following problem, which arises in connection with semantic inference of arity larger than two: can every multivariate non-decreasing real function be expressed as a composition of non-decreasing real functions in two variables?
Cite as

Yuval Filmus, Pavel Hrubeš, and Massimo Lauria. Semantic Versus Syntactic Cutting Planes. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 35:1-35:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.STACS.2016.35,
  author =	{Filmus, Yuval and Hrube\v{s}, Pavel and Lauria, Massimo},
  title =	{{Semantic Versus Syntactic Cutting Planes}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{35:1--35:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.35},
  URN =		{urn:nbn:de:0030-drops-57367},
  doi =		{10.4230/LIPIcs.STACS.2016.35},
  annote =	{Keywords: proof complexity, cutting planes, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.433
The Space Complexity of Cutting Planes Refutations

Authors: Nicola Galesi, Pavel Pudlák, and Neil Thapen

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We study the space complexity of the cutting planes proof system, in which the lines in a proof are integral linear inequalities. We measure the space used by a refutation as the number of linear inequalities that need to be kept on a blackboard while verifying it. We show that any unsatisfiable set of linear inequalities has a cutting planes refutation in space five. This is in contrast to the weaker resolution proof system, for which the analogous space measure has been well-studied and many optimal linear lower bounds are known. Motivated by this result we consider a natural restriction of cutting planes, in which all coefficients have size bounded by a constant. We show that there is a CNF which requires super-constant space to refute in this system. The system nevertheless already has an exponential speed-up over resolution with respect to size, and we additionally show that it is stronger than resolution with respect to space, by constructing constant-space cutting planes proofs, with coefficients bounded by two, of the pigeonhole principle. We also consider variable instance space for cutting planes, where we count the number of instances of variables on the blackboard, and total space, where we count the total number of symbols.
Cite as

Nicola Galesi, Pavel Pudlák, and Neil Thapen. The Space Complexity of Cutting Planes Refutations. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 433-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{galesi_et_al:LIPIcs.CCC.2015.433,
  author =	{Galesi, Nicola and Pudl\'{a}k, Pavel and Thapen, Neil},
  title =	{{The Space Complexity of Cutting Planes Refutations}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{433--447},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.433},
  URN =		{urn:nbn:de:0030-drops-50551},
  doi =		{10.4230/LIPIcs.CCC.2015.433},
  annote =	{Keywords: Proof Complexity, Cutting Planes, Space Complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2014.325
Partition Expanders

Authors: Dmitry Gavinsky and Pavel Pudlák

Published in: LIPIcs, Volume 25, 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)

Abstract
We introduce a new concept, which we call partition expanders. The basic idea is to study quantitative properties of graphs in a slightly different way than it is in the standard definition of expanders. While in the definition of expanders it is required that the number of edges between any pair of sufficiently large sets is close to the expected number, we consider partitions and require this condition only for most of the pairs of blocks. As a result, the blocks can be substantially smaller. We show that for some range of parameters, to be a partition expander a random graph needs exponentially smaller degree than any expander would require in order to achieve similar expanding properties. We apply the concept of partition expanders in communication complexity. First, we give a PRG for the SMP model of the optimal seed length, n+O(log(k)). Second, we compare the model of SMP to that of Simultaneous Two-Way Communication, and give a new separation that is stronger both qualitatively and quantitatively than the previously known ones.
Cite as

Dmitry Gavinsky and Pavel Pudlák. Partition Expanders. In 31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 25, pp. 325-336, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{gavinsky_et_al:LIPIcs.STACS.2014.325,
  author =	{Gavinsky, Dmitry and Pudl\'{a}k, Pavel},
  title =	{{Partition Expanders}},
  booktitle =	{31st International Symposium on Theoretical Aspects of Computer Science (STACS 2014)},
  pages =	{325--336},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-65-1},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{25},
  editor =	{Mayr, Ernst W. and Portier, Natacha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2014.325},
  URN =		{urn:nbn:de:0030-drops-44684},
  doi =		{10.4230/LIPIcs.STACS.2014.325},
  annote =	{Keywords: partitions, expanders, communication, complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.30
On extracting computations from propositional proofs (a survey)

Authors: Pavel Pudlák

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
This paper describes a project that aims at showing that propositional proofs of certain tautologies in weak proof system give upper bounds on the computational complexity of functions associated with the tautologies. Such bounds can potentially be used to prove (conditional or unconditional) lower bounds on the lengths of proofs of these tautologies and show separations of some weak proof systems. The prototype are the results showing the feasible interpolation property for resolution. In order to prove similar results for systems stronger than resolution one needs to define suitable generalizations of boolean circuits. We will survey the known results concerning this project and sketch in which direction we want to generalize them.
Cite as

Pavel Pudlák. On extracting computations from propositional proofs (a survey). In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 30-41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{pudlak:LIPIcs.FSTTCS.2010.30,
  author =	{Pudl\'{a}k, Pavel},
  title =	{{On extracting computations from propositional proofs (a survey)}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{30--41},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.30},
  URN =		{urn:nbn:de:0030-drops-28512},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.30},
  annote =	{Keywords: proof complexity, propositional tautology, boolean circuits, resolution, feasible interpolation}
}
Document
DOI: 10.4230/DagSemProc.06111.2
06111 Executive Summary – Complexity of Boolean Functions

Authors: Matthias Krause, Dieter van Melkebeek, Pavel Pudlák, and Rüdiger Reischuk

Published in: Dagstuhl Seminar Proceedings, Volume 6111, Complexity of Boolean Functions (2006)

Abstract
We briefly describe the state of the art concerning the complexity of discrete functions. Computational models and analytical techniques are summarized. After describing the formal organization of the Dagstuhl seminar "Complexity of Boolean Functions" held in March 2006, we introduce the different topics that have been discussed there and mention some of the major achievements. The summary closes with an outlook on the development of discrete computational complexity in the future.
Cite as

Matthias Krause, Dieter van Melkebeek, Pavel Pudlák, and Rüdiger Reischuk. 06111 Executive Summary – Complexity of Boolean Functions. In Complexity of Boolean Functions. Dagstuhl Seminar Proceedings, Volume 6111, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{krause_et_al:DagSemProc.06111.2,
  author =	{Krause, Matthias and van Melkebeek, Dieter and Pudl\'{a}k, Pavel and Reischuk, R\"{u}diger},
  title =	{{06111 Executive Summary – Complexity of Boolean Functions}},
  booktitle =	{Complexity of Boolean Functions},
  pages =	{1--5},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6111},
  editor =	{Matthias Krause and Pavel Pudl\'{a}k and R\"{u}diger Reischuk and Dieter van Melkebeek},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.06111.2},
  URN =		{urn:nbn:de:0030-drops-8409},
  doi =		{10.4230/DagSemProc.06111.2},
  annote =	{Keywords: Boolean and quantum circuits, discrete problems, computational complexity, lower bounds, communication complexity, proof and query complexity, randomization, pseudo-randomness, derandomization, approximation, cryptography, computational learning}
}
  • Refine by Author
  • 12 Pudlák, Pavel
  • 3 Khaniki, Erfan
  • 3 Talebanfard, Navid
  • 3 Thapen, Neil
  • 2 Krause, Matthias
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 6 proof complexity
  • 2 communication complexity
  • 2 computational complexity
  • 2 cryptography
  • 2 derandomization
  • Show More...

  • Refine by Type
  • 17 document

  • Refine by Publication Year
  • 3 2017
  • 3 2024
  • 2 2006
  • 2 2022
  • 1 2003
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact