Описывается атака на блочные шифры, основанная на известной концепции «встреча посередине». В рамках предлагаемой атаки для решения уравнений криптоанализа используются алгоритмы решения проблемы булевой выполнимости. Основное нововведение заключается в том, что в пропозициональной кодировке шифра учитывается информация не только от прямых, но и от обратных раундовых преобразований. Для ряда сокращённых по числу раундов блочных шифров построены оценки трудоёмкости атак из класса «угадывай и определяй» с использованием нового принципа кодирования. В некоторых случаях новые атаки оказались в разы эффективнее аналогов, в которых используются стандартные методы кодирования.