Санкт-петербургский национальный исследовательский

Minisat [5] – минималистичный ​SAT
​
-решатель с открытым исходным
кодом. Обладает наградами ряда соревнований ​SAT Competition [6]. Его
 
авторами были выделены следующие ключевые особенности: 
12 

---

1. Простота модификации, которая достигается благодаря хорошей
документации, а также продуманности и простоте его строения. 
2. Высокая эффективность, которую доказывают награды, полученные
на соответствующих соревнованиях. 
3. Нацеленность на интеграцию в качестве модуля. 
Lingeling [7] – серьезный инструмент для решения задач булевой
выполнимости. Является обладателем множества различных наград таких
соревнований как: SAT Competition [6], ​SAT Race
​
, ​Configurable SAT Solver
 
 
 
 
 
 
Challenge (​CSSC’14
​
) [8]. Имеет более сотни настраиваемых параметров,
что позволяет хорошо адаптироваться к решению различных классов
задач. Также имеет интерфейс для запуска в многопоточном режиме –
Plingeling
​
, и параллельный решатель на основе сочетания методов ​Cube &

Conquer
​
и ​Сonflict-Driven Clause Learning
​
(​CDCL
​
) [9] – ​Treengeling
​
.
ROKK [10] – модифицированная версия ​SAT
​
-решателя ​Minisat
​
.
Состоит из двух компонентов: ​SATELite [11] и, собственно, ​Minisat
​
.
Первый компонент осуществляет упрощение решаемой ​SAT
​
-задачи, после
чего упрощенная КНФ передается в модуль ​Minisat
​
, который описан выше,
для дальнейшего решения. 
В
данной
работе
используются
все
рассмотренные
выше
SAT
​
-решатели. Одной из особенностей программной среды является
возможность
простого
переключения
между
используемыми
SAT
​
-решателями, а также добавления новых.