Steklov Institute of Mathematics at St.Petersburg

PREPRINT 12/2015

SIMULTANEOUS SEPARATION OF REGULAR RESOLUTION, TREELIKE RESOLUTION AND EXPONENT OF RESOLUTION DEPTH

This preprint was accepted December 17, 2015

ABSTRACT:  Every unsatisfiable CNF formula $\phi$ has the following parameters: the size of the minimal regular resolution proof $S_R(\phi)$, the size of the minimal treelike resolution proof $S_T(\phi)$, the minimal depth of a resolution proof $d(\phi)$. The following inequality is trivially satisfied: $2^{d(\phi)}\ge S_T(\phi)\ge S_R(\phi)$. Bonet, Esteban,  Galesi and Johannsen in 2000 showed that there exists family of formulas $F_n$ such that $S_T(F_n)=2^{\Omega(\sqrt{S_R(F_n)})}$. Urquhart in 2011 gave a family of 3-CNF formulas $H_n$ such that $S_T(H_n)=O(n)$ and $d(H_n)=\Omega(n/\log n)$.

We observe that formulas $H^{\oplus}_n$ which is the xorification of $H_n$ has $S_T(H^{\oplus}_n)=2^{\Omega(n/\log n)}$ and $S_R(H^{\oplus}_n)=O(n)$; this improves the separation given by Bonet et al. 

We present a family of 6-CNF formulas $\Phi_n$ such that any two values from $\{2^{d(\Phi_n)}, S_T(\Phi_n), S_R(\Phi_n)\}$ differ superpolynomially. Our formulas are based on the Pebbling contradictions on the $n\times n$ square graph. Our proof is elementary and is based on the game interpretation of the resolution depth and the xorification. 
   

Д. М. ИЦЫКСОН

ОДНОВРЕМЕННОЕ РАЗДЕЛЕНИЕ РЕГУЛЯРНОЙ РЕЗОЛЮЦИИ, ДРЕВОВИДНОЙ РЕЗОЛЮЦИИ И ЭКСПОНЕНТЫ ОТ РЕЗОЛЮЦИОННОЙ ГЛУБИНЫ

АННОТАЦИЯ   Каждой невыполнимой формуле в КНФ $\phi$ соответсвуют следующие параметры: размер минимального регулярного резолюционного доказательства $S_R(\phi)$, размер минимального древовидного резолюционного доказательства $S_T(\phi)$, минимальная глубина резолюционного доказательства $d(\phi)$. Следующее неравенство выполняется по тривиальным причинам: $2^{d(\phi)}\ge S_T(\phi)\ge S_R(\phi)$. Боне, Эстебан, Галези и Йохансен в 2000 году показали, что существует такая последовательность формул $F_n$, что  $S_T(F_n)=2^{\Omega(\sqrt{S_R(F_n)})}$. Уркарт в 2011 году предложил семейство 3КНФ формул $H_n$, что $S_T(H_n)=O(n)$ и $d(H_n)=\Omega(n/\log n)$. 

Мы замечаем, что формулы $H^{\oplus}_n$, которые являются ксорификацией формул $H_n$ имеют $S_T(H^{\oplus}_n)=2^{\Omega(n/\log n)}$ и $S_R(H^{\oplus}_n)=O(n)$; это усиливает разделение Боне и др. 

Мы строим семейство формул в 6-КНФ $\Phi_n$, что любые две величины из $\{2^{d(\Phi_n)}, S_T(\Phi_n), S_R(\Phi_n)\}$ отличаются суперполиномиально. Наши формулы основаны на игре с фишками на графе квадрата $n\times n$. Наше доказательство элементарно и основано на игровой интерпретации глубины и ксорификации.