Алгоритмы решения проблемы булевой выполнимости (SAT – от Satisfiability) и реализующие их средства (SAT-решатели) позволяют определить выполнимость конкретной булевой формулы – существует ли такой набор определенных булевых значений («ложь»/«истина») переменных формулы, при которых результат…