Работа представляет собой SatSolver. На вход подается cnf, в ответ выходит или unsat, или sat с приложением одной модели
Clause - "предложение", представляет собой дизъюнкцию литералов Cnf - конъюнкция Clause
1.Находим литерал с одной полярностью, после чего удаляем все предложения с ним (метод EliminatePureLiteral). Заносим в модель этот литерал со значением true, если полярность "положительная", иначе - false
2.Находим предложения с одним литералом и удаляем их. Также удаляем предложения, где встречается этот литерал с "положительной" полярностью, иначе - удаляем этот литерал (метод InsertValueToLiteral)
3.Берем случайный литерал и вставляет в него два значения
Алгоритм завершается "успешно", если не остается clause
Алгоритм выдает unsat, если есть пустая clause