On the Dominance-Based Strengthening Rule

Channel:
United States Simons Institute for the Theory of Computing
Subscribers:
68,700
Published on ● Video Link: https://www.youtube.com/watch?v=IdAlFBFDzKk


Duration: 32:51
346 views
3

Neil Thapen (Institute of Mathematics, Czech Academy of Sciences)
https://simons.berkeley.edu/talks/neil-thapen-institute-mathematics-czech-academy-sciences-2023-03-23-0
Proof Complexity and Meta-Mathematics

[Bogaerts, Gocht, McCreesh, Nordstrom, AAII-22] introduces a proof system which can be thought of as extended Frege plus a novel "dominance-based strengthening rule", as a tool to certify correctness of runs of a symmetry-breaking SAT solver. We observe that this rule simulates, in a certain sense, polynomial local search and thus show, via known results in bounded arithmetic, that the system is equivalent to the quantified propositional proof system G_1. As such it is likely to be strictly stronger than extended Frege. This is joint work with Leszek Kolodziejczyk.



Other Videos By Simons Institute for the Theory of Computing


2023-03-27In Search of the Ideal: Toni Pitassi and her work on Algebraic Proof Systems
2023-03-25TFNP
2023-03-25Lower Bounds for NW-generators in AC0-Frege
2023-03-25Implicit Proof Systems
2023-03-24Unprovability and Other Impossibility Results in Machine Learning
2023-03-24Weak Versions of Extended Resolution
2023-03-24CDCL vs Resolution: The Picture in QBF
2023-03-24Read-Once Branching Programs as Proof Lines
2023-03-24Connections Between QBF Proof Complexity and Circuit Complexity
2023-03-24Certifying Combinatorial Solving Using Cutting Planes with Strengthening Rules
2023-03-24On the Dominance-Based Strengthening Rule
2023-03-23On the Problems Related to Waring Rank and Border Waring Rank
2023-03-23Lower Bounds Against Non-Commutative Models of Algebraic Computation
2023-03-23Natural Proofs in Algebraic Circuit Complexity
2023-03-23Variety Membership Testing, Algebraic Natural Proofs, and Geometric Complexity Theory
2023-03-22Frontiers of Proof Complexity Lower Bounds via Algebraic Complexity & Open Problems
2023-03-22Indistinguishability Obfuscation via Mathematical Proofs of Equivalence
2023-03-22Towards P≠NP from Extended Frege Lower Bounds
2023-03-22Indistinguishability Obfuscation, Range Avoidance, and Bounded Arithmetic
2023-03-22Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic
2023-03-21Consistency of NEXP Not in P/poly in a Strong Theory


Tags:
Simons Institute
theoretical computer science
UC Berkeley
Computer Science
Theory of Computation
Theory of Computing
Proof Complexity and Meta-Mathematics
Neil Thapen