Tata Institute of Fundamental Research
How Limited Interaction Hinders Real Communication (and What it Means for Proof and Circuit Complexity)
STCS Seminar
Speaker:
Marc Vinyals (KTH Royal Institute of Technology
School of Computer Science and Communication
Lindstedtsvagen 5
D Building, 4518
Sweden)
Organiser:
Arkadev Chattopadhyay
Date:
Tuesday, 14 Feb 2017, 16:00 to 17:00
Venue:
A-201 (STCS Seminar Room)
(Scan to add to calendar)
Abstract:
Nowadays SAT solvers are able to solve problems with millions of variables, but some instances are still hard. While some formulas just require large time or memory to solve, other formulas allow to trade these resources. In the language of proof complexity, they have both short proofs and proofs in small space, but optimizing either measure blows up the other.
In this talk we will look at size-space trade-offs that hold not only for the resolution proof system, which captures most current solvers, but for polynomial calculus and cutting planes, which capture algebraic and pseudo-boolean reasoning respectively. The proof goes through communication complexity, and a key insight is to use a model of communication that captures short cutting planes proofs: communication with limited rounds and with real numbers (joint work with Susanna F. de Rezende and Jakob Nordström).
| Speaker: | Marc Vinyals (KTH Royal Institute of Technology School of Computer Science and Communication Lindstedtsvagen 5 D Building, 4518 Sweden) |
| Organiser: | Arkadev Chattopadhyay |
| Date: | Tuesday, 14 Feb 2017, 16:00 to 17:00 |
| Venue: | A-201 (STCS Seminar Room) |
(Scan to add to calendar)
Abstract:
Nowadays SAT solvers are able to solve problems with millions of variables, but some instances are still hard. While some formulas just require large time or memory to solve, other formulas allow to trade these resources. In the language of proof complexity, they have both short proofs and proofs in small space, but optimizing either measure blows up the other.
In this talk we will look at size-space trade-offs that hold not only for the resolution proof system, which captures most current solvers, but for polynomial calculus and cutting planes, which capture algebraic and pseudo-boolean reasoning respectively. The proof goes through communication complexity, and a key insight is to use a model of communication that captures short cutting planes proofs: communication with limited rounds and with real numbers (joint work with Susanna F. de Rezende and Jakob Nordström).
In this talk we will look at size-space trade-offs that hold not only for the resolution proof system, which captures most current solvers, but for polynomial calculus and cutting planes, which capture algebraic and pseudo-boolean reasoning respectively. The proof goes through communication complexity, and a key insight is to use a model of communication that captures short cutting planes proofs: communication with limited rounds and with real numbers (joint work with Susanna F. de Rezende and Jakob Nordström).