Мы рассматриваем алгоритмы для SAT, которые могут расщепляться по значениям линейных равенств по модулю 2. Например, в одной ветви он может рассматривать случай, что x+y+z=0, а в другой, что x+y+z=1. Будет рассказана экспоненциальная нижняя оценка на время работы всех таких алгоритмов для формул, кодирующих принцип Дирихле. Доказательство этого результата элементарно. Также мы поговорим о связанных с этим алгоритмом системах доказательств (аналог метода резолюций, но работающий с линейными равенствами вместо литералов), для таких систем доказательств мы докажем полиномиальную эквивалентность семантической и синтаксической версии и импликационную полноту.

Летом 2013 года Дима рассказывал нижнюю оценку через коммуникационную сложность. Если останется время, то я расскажу предложенное А. Шенем упрощенное изложение Диминого результата. Доклад не будет зависить от предыдущего Диминого доклада и никаких предварительных знаний не требуется. В конце будет сформулировано несколько открытых вопросов, среди них есть те, которые реально закрыть.