Изменения
Small fix
== Общие соображения ==
* В каждой $s_i$ ровно $m$ переменных с отрицанием и столько же без него.
* Каждой $s_i$ можно однозначно сопоставить в пару такую $s_j$ такую, что все переменные с отрицанием из $s_i$ в $s_j$ будут без отрицания и наоборот. Это следует из того, как мы строим набор ${s_i}$ {{---}} циклически сдвигаем "крышу отрицания" над переменными, пока не получим все такие. Для нахождения нужно сдвинуть "крышу" ровно на $m$ позиций (вправо или влево, это не важно {{---}} получится одно и то же). Назовем такую пару $(s_i, s_j)$ двойственной, и пусть $s_j = \neg s_i$ (на самом деле $\neg s_i = s_{i+m}$). * Назовем '''самостоятельной единицей''' для $s_i$ любой ее единичный аргумент (с учетом возможных отрицаний). То есть если $x_j = 1$ и в $s_i$ он стоит без отрицания, то это будет самостоятельная единица. Также $a_jx_j$ будет самостоятельной единицей, если $a_j x_j = 0$ и в $s_i$ он стоит с отрицанием. В остальных случаях $a_jx_j$ не является самостоятельной единицей.* Если самостоятельных единиц в $s_i$ "достаточно много" (а сколько именно, будет зависеть от $x_0$), то в $\neg s_i$ их будет "достаточно мало".
{{Утверждение
Таким образом, сделав $m$ шагов, мы дойдем от $s_l$ до $\neg s_l$, причем количество единиц в $A_l$ будет изменяться не более, чем на $1$. Изначально оно было $a_l$, а станет {{---}} $2t - a_l$.
Тогда выполняются неравенства: $a_k \le t \le 2t - a_k$. Левый знак верен просто потому, что мы так выбрали $s_k$, а правый, очевидно, равносилен первому.
Таким образом, мы, изменяя $a_l $ не больше, чем на единицу, пришли из $a_k$ в $2t - a_k$, причем число $t$ было между ними. Поэтому мы обязательно на каком-то шаге оказались с $a_{l'} = t$, то есть ровно половина единиц попала в $A_{l'}$, чего мы и хотели.
Заметим также, что мы доказали наличие '''одной пары''', но на самом деле таких может быть больше. Давайте такие пары назовем '''особенными''', а остальные {{---}} обычными.
}}
