Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2017 | Book

Introduction Read chapter Read first chapter

Space in Weak Propositional Proof Systems

Author: Dr. Ilario Bonacina

Publisher: Springer International Publishing

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book considers logical proof systems from the point of view of their space complexity. After an introduction to propositional proof complexity the author structures the book into three main parts. Part I contains two chapters on resolution, one containing results already known in the literature before this work and one focused on space in resolution, and the author then moves on to polynomial calculus and its space complexity with a focus on the combinatorial technique to prove monomial space lower bounds. The first chapter in Part II addresses the proof complexity and space complexity of the pigeon principles. Then there is an interlude on a new type of game, defined on bipartite graphs, essentially independent from the rest of the book, collecting some results on graph theory. Finally Part III analyzes the size of resolution proofs in connection with the Strong Exponential Time Hypothesis (SETH) in complexity theory.

The book is appropriate for researchers in theoretical computer science, in particular computational complexity.

Table of Contents

Frontmatter
Chapter 1. Introduction
Abstract
This chapter is a general introduction to some of the themes of propositional proof complexity. We introduce on a high level proof systems such as resolution and polynomial calculus, we recall some connections between proof complexity and SAT algorithms, and we introduce on a high level the topic of space in propositional proof systems. We conclude with a summary of the results shown in this book.
Ilario Bonacina

General Results and Techniques

Frontmatter
Chapter 2. Resolution
Abstract
In this chapter we recall some basic general facts about the proof complexity of resolution [Bla37, Rob65]. This will be a common background for the results in Chap. 3 and Chap. 8. First we describe the most common restrictions placed on the type of resolution refutations, that is regular and tree-like resolution refutations (Sect. 2.1), then we prove a non-trivial size upper bound (Sect. 2.2) and finally we move to the complexity measures known as width and asymmetric width (Sect. 2.3).
Ilario Bonacina
Chapter 3. Space in Resolution
Abstract
In this chapter we investigate the space complexity of resolution in particular from the point of view of the total space measure, see Sect. 3.3.We briefly review results about the clause space (Sect. 3.2) and the variable space measures (Sect. 3.4). We prove a general inequality between the total space measure and width, Theorem 3.6. Then, when talking about space it is natural to introduce a semantic version of resolution, see Sect. 3.1. We show the separation of resolution and semantic resolution and also a technique to prove total space lower bounds in semantic resolution, Theorem 3.7, and a bounded version of it, Theorem 3.8.
Ilario Bonacina
Chapter 4. Space in Polynomial Calculus
Abstract
In this chapter we consider in detail the propositional proof system polynomial calculus, briefly introduced in Sect. 1.1.2. We introduce some complexity measures—size, degree, monomial space and total space—and we show some techniques useful to prove lower bounds on those.
Ilario Bonacina

Applications

Frontmatter
Chapter 5. Pigeonhole Principles
Abstract
The pigeonhole principle asserts that there is no multi-valued total injective mapping from a set with m elements into a set with n elements, if m > n. The elements of the set of size m are traditionally called pigeons and the elements of the set of size n are called holes and so the pigeonhole principle can be stated more pictorially saying that
if m > n pigeons fly to n holes then (at least) two of them must go to the same hole.
Ilario Bonacina
Chapter 6. Interlude: Cover Games
Abstract
Let’s put aside proof complexity for a moment and, in this chapter, we will focus on some properties of bipartite graphs.
Ilario Bonacina
Chapter 7. Some Graph-Based Formulas
Abstract
We now show some further applications of the general theorems to prove space lower bounds from Chap. 3 and Chap. 4. That is we see how to prove monomial and resolution total space lower bounds for random k-CNF formulas (Sect. 7.2), the pigeonhole principle over a bipartite graph (Sect. 7.3) and Tseitin formulas (Sect. 7.4).
Ilario Bonacina

A Postlude

Frontmatter
Chapter 8. Strong Size Lower Bounds for (a Subsystem of) Resolution
Abstract
In this chapter we put the spotlight again on resolution size and in particular on its connection with conjectures about the exact complexity of the k-SAT problem, that is the conjectures known as the Exponential Time Hypothesis (ETH) and the Strong Exponential Time Hypothesis (SETH). We show a strong width lower bound (Theorem 8.1) and a strong size lower bound for a subsystem of resolution. The lower bounds are stronger than the one we could get immediately from the size-width inequality, eq. (2.10).
Ilario Bonacina
Backmatter
Metadata
Title
Space in Weak Propositional Proof Systems
Author
Dr. Ilario Bonacina
Copyright Year
2017
Electronic ISBN
978-3-319-73453-8
Print ISBN
978-3-319-73452-1
DOI
https://doi.org/10.1007/978-3-319-73453-8

Premium Partner

    Image Credits