Search Results

Documents authored by 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
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/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.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}
}
Document
DOI: 10.4230/DagSemProc.06111.1
06111 Abstracts Collection – Complexity of Boolean Functions

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

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

Abstract
From 12.03.06 to 17.03.06, the Dagstuhl Seminar 06111 ``Complexity of Boolean Functions'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

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

Copy BibTex To Clipboard

@InProceedings{krause_et_al:DagSemProc.06111.1,
  author =	{Krause, Matthias and Pudl\'{a}k, Pavel and Reischuk, R\"{u}diger and van Melkebeek, Dieter},
  title =	{{06111 Abstracts Collection – Complexity of Boolean Functions}},
  booktitle =	{Complexity of Boolean Functions},
  pages =	{1--24},
  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.1},
  URN =		{urn:nbn:de:0030-drops-7593},
  doi =		{10.4230/DagSemProc.06111.1},
  annote =	{Keywords: Complexity of Boolean functions, Boolean circuits, binary decision diagrams, lower bound proof techniques, combinatorics of Boolean functions, communi algorithmic learning, cryptography, derandomization}
}
Document
DOI: 10.4230/DagSemRep.374
The Propositional Satisfiability Problem -- Algorithms and Lower Bounds (Dagstuhl Seminar 03141)

Authors: Andreas Goerdt, Pavel Pudlák, Uwe Schöning, and Osamu Watanabe

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Andreas Goerdt, Pavel Pudlák, Uwe Schöning, and Osamu Watanabe. The Propositional Satisfiability Problem -- Algorithms and Lower Bounds (Dagstuhl Seminar 03141). Dagstuhl Seminar Report 374, pp. 1-5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{goerdt_et_al:DagSemRep.374,
  author =	{Goerdt, Andreas and Pudl\'{a}k, Pavel and Sch\"{o}ning, Uwe and Watanabe, Osamu},
  title =	{{The Propositional Satisfiability Problem -- Algorithms and Lower Bounds (Dagstuhl Seminar 03141)}},
  pages =	{1--5},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{374},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.374},
  URN =		{urn:nbn:de:0030-drops-152545},
  doi =		{10.4230/DagSemRep.374},
}
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 Imprint Privacy Contact