08/07/2020

Feasible Interpolation for Polynomial Calculus and Sums-of-Squares

Tuomas Hakoniemi

Keywords: Proof Complexity, Feasible Interpolation, Sums-of-Squares, Polynomial Calculus

Abstract Paper Similar Papers

Abstract: We prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x,z) and Q(y,z) of equality constraints, a refutation Π of P(x,z) ∪ Q(y,z), and any assignment a to the variables z, one can find a refutation of P(x,a) or a refutation of Q(y,a) in time polynomial in the length of the bit-string encoding the refutation Π. For Sums-of-Squares we rely on the use of Boolean axioms, but for Polynomial Calculus we do not assume their presence.

 0
 0
 0
 0
  Share    
This is an embedded video. Talk and the respective paper are published at ICALP 2020 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd Characters remaining: 140

Similar Papers

 0
 0
 0
 0
 23:36 
 0
 0
 0
 0
 16:26 
 0
 0
 0
 0
 16:22 
 0
 0
 0
 0
 20:17 
 0
 0
 0
 0
 23:56 
 0
 0
 0
 0
 17:41 
 0
 0
 0
 0
 28:27 
 0
 0
 0
 0
 22:19 
 0
 0
 0
 0
 14:51 
 0
 0
 0
 0
 24:19 
 0
 0
 0
 0
 25:11 
 0
 0
 0
 0
 19:36 
 0
 0
 0
 0
 22:14 
 0
 0
 0
 0
 19:39 
 0
 0
 0
 0
 23:03 
 0
 0
 0
 0
 19:57 
 0
 0
 0
 0
 15:02 
 0
 0
 0
 0
 19:01 
 0
 0
 0
 0
 14:09 
 0
 0
 0
 0
 2:54 
 0
 0
 0
 0
 24:54 
 0
 0
 0
 0
 21:02 
 0
 0
 0
 0
 16:06 
 0
 0
 0
 0
 12:11 
 0
 0
 0
 0
 30:00 
 0
 0
 0
 0
 3:33 
 1
 1
 0
 0
 9:31 
 0
 0
 0
 0
 25:48 
 0
 0
 0
 0
 13:34 
 0
 0
 0
 0
 16:53 
 0
 0
 0
 0
 12:42 
 0
 0
 0
 0
 24:20 
 0
 0
 0
 0
 23:49 
 0
 0
 0
 0
 24:02 
 0
 0
 0
 0
 14:53 
 0
 0
 0
 0
 15:40 
 0
 0
 0
 0
 24:00 
 0
 0
 0
 0
 8:35 
 0
 0
 0
 0
 26:16 
 0
 0
 0
 0
 10:59