Полиномиальный в среднем алгоритм для SAT