Многопоточный решатель проблемы MaxSAT

Программа предназначена для решения задач максимальной булевой выполнимости (MaxSAT) с применением методов локального поиска. Основная новизна состоит в использовании принципа склеивания переменных. В данной метаэвристике выполняется объединение булевых переменных, над которыми построена КНФ, в «склеенные» переменные. Декартово произведения доменов склеенных переменных – это метрическое пространство с метрикой Хэмминга. Решатель выполняет локальный поиск для сопряженной функции в новом пространстве. Для выхода из локальных экстремумов применяются различные варианты эволюционных эвристик. При длительных стагнациях строится новое множество склеенных переменных. Программа разработана при поддержке совета по грантам Президента Российской Федерации (стипендия СП-3545.2019.5) и в рамках госзадания по проекту FWEW-2021-0003 (№ гос регистрации: 121041300065-9)