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

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