Аннотация:
В работе приводятся алгоритмы построения декомпозиционных множеств, используемых для крупноблочного распараллеливания SAT-задач и их последующего решения в распределенных вычислительных средах. В основе предлагаемых алгоритмов лежит вычислительная схема метода Монте-Карло.