Home - gromas/polysat GitHub Wiki

Задача определения выполнимости пропозициональных булевых формул (k-SAT) является одной из важных задач теории сложности вычислений. Ответ на вопрос, можно ли получить решение так же быстро, как и проверить его, может дать толчок в развитии систем принятия и проверки решений, автоматизированного проектирования, разработки программ и средств защиты информации.

Целью настоящего проекта является разработка алгоритма, позволяющего решать задачи выполнимости 3-SAT за полиномиальное время и пространство на обычном компьютере.