Параллельный решатель задач булевой выполнимости HPCSAT

Программа предназначена для параллельного решения ресурсоемких задач булевой выполнимости большой размерности на вычислительных кластерах с SMP-узлами и ориентирована на применение при проведении вычислительных экспериментов в различных предметных областях, где в процессе исследований возникают дискретные модели в виде систем булевых уравнений. Программа представляет собой масштабируемое MPI-приложение на языке С . Главный процесс приложения организует динамическую очередь подзадач, получаемых в результате декомпозиции исходной булевой модели методом расщепления. В дочернем процессе может выполняться как многопоточное, так и однопоточное приложение. Программа реализована на основе метода полного поиска и использует параллелизм по данным. Пользователю предоставляется возможность выбора эвристики расщепления, глубины расщепления и базового решателя, запускаемого в дочернем процессе.