Изменения
Нет описания правки
Хотелось бы воспользоваться протоколом из [[Sharp SAT|доказательства принадлежности #SAT к классу IP]], проверяя <tex>A_i(1)\cdot A_i(0)=A_{i-1}(r_{i})</tex> в случае, когда <tex>x_i</tex> связан квантором <tex>\forall</tex>, и <tex>A_i(1)+A_i(0)=A_{i-1}(r_{i})</tex> для квантора <tex>\exists</tex>. К сожалению, сразу этот протокол применить нельзя, потому что произведение может увеличить степень полинома в два раза, а это может потребовать передачи по протоколу полиномов экспоненциальной длины, что не уложится по времени.
Поэтому потребуем, чтобы между появлением переменной и первым ее использованием было не более одного квантора <tex>\forall</tex>. Для этого заменим все суффиксы вида <tex>\forall x_{i+1} \tau(x_1, x_2, \ldots, x_i, x_{i+1})</tex> на <tex>\forall x_{i+1} \exists x_1',\ldots,x_i'(x_1=x_1')\land(x_2=x_2')\land \ldots \land(x_i=x_i')\land \tau(x_1', x_2', \ldots, x_i', x_{i+1})</tex>. Это преобразование не изменит выполнимости формулы, количество ее переменных увеличится лишь в полином от их первоначального количества раз, а сама формула тоже увеличится не более, чем полиномиально. Теперь можно использовать протокол из [[Sharp SAT|#SAT]]для получившейся формулы, передаваться будут полиномы константной степени.
