• Fedor Part
    • (Royal Holloway, University of London)
    • Lower Bounds for Resolution with Linear Equations over a Ring
    • Abstract:
    • The proof system Res(lin_R) is an extension of Resolution in which proof lines are disjunctions of linear equations over a ring R. If R is a finite field GF(p), Res(lin_R) can be viewed as a "minimal" fragment of bounded depth Frege system with counting gates AC^0[p]-Frege (and similarly, for R the integers and the TC^0-Frege), for which no nontrivial lower bound is known. Recent suggested approaches for obtaining lower bounds against Res(lin_GF(2)) refutations include feasible interpolation and combinatorial techniques. In this talk we explore and develop further the combinatorial approach for various rings R. In particular, we prove an exponential-size dag-like Res(lin_F) lower bound for the Subset Sum principle with large coefficients, as well as establish a host of new tree-like lower bounds and separations over different fields. Based on a joint work with Iddo Tzameret.
    • 17.12.18   14:00
    • Neil Thapen
    • (Institute of Mathematics)
    • DRAT proofs without new variables
    • Abstract:
    • The DRAT proof system is used by modern SAT solvers to witness that a CNF is unsatisfiable. The full system allows you to freely introduce new variables, and is as strong as extended resolution. I will discuss some upper and lower bounds on a restricted system, in which you cannot introduce new variables. This is ongoing work with Sam Buss.
    • 10.12.18   14:00

    Pavel Pudlak, Neil Thapen