
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^0Frege), 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 exponentialsize daglike Res(lin_F) lower bound for the Subset Sum principle with large coefficients, as well as establish a host of new treelike lower bounds and separations over different fields. Based on a joint work with Iddo Tzameret.

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.
Pavel Pudlak, Neil Thapen
organizers