Iedereen is welkom voor de N&O lezing van Samarth Tiwari met als titel 'On the Complexity of Branching Proofs'
via zoom:
https://us02web.zoom.us/j/89018344147
Abstract:
Certifying that a polytope contains no integer points is of central importance in proof complexity and integer programming. Among the various systems for generating such certificates, we consider the system of branching proofs. Recently, Beame et al (ITCS 2018) asked whether the bit size of the coefficients in a branching proof, which they named stabbing planes (SP) refutations, can be assumed to be polynomial in n for polytopes derived from SAT formulas.
This talk will introduce notions of proof complexity and motivate this problem, then sketch our resolution of this question of Beame et al.
We laten een techniek zien om elk vertakkingsbewijs opnieuw te compileren zodat de integer-disjuncties maximaal coëfficiënten hebben (nR) ^ {O (n ^ 2)}, waarbij R een positief geheel getal is zodat K in een l_1 bol met straal R ligt , terwijl het aantal knooppunten in de vertakkende boom met maximaal een factor O (n) wordt vergroot.
Ten tweede zijn Tseitin-formules een klasse van onhaalbare SAT- gevallen die als een belangrijk voorbeeld dienen voor het bestuderen van de kracht van verschillende bewijssystemen. We zullen laten zien dat Tseitin-formules quasi-polynomiale snijvlak (CP) weerleggingen hebben, wat het vermoeden weerlegt dat Tseitin-formules (exponentieel) moeilijk zijn voor CP.
