![Meta-complexity_logo_hi-res](/sites/default/files/styles/workshop_banner_sm_1x/public/2023-02/Meta-complexity_hi-res.png.jpg?itok=oFqprXq1)
Abstract
[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.