Разделение и / или разбиение большого файла CNF / Matrix
Простой вопрос У меня есть очень большой файл CNF с представляет матрицу MXN. допустим,>10000 переменных с соответствующими терминами. Итак, в качестве первого шага я хочу разделить файл CNF или, что еще лучше, разбить матрицу на переменные 100 для параллельного решения концепций. Есть ли описание, какие правила применять?
Вся помощь приветствуется.
С уважением Адриан
1 ответ
Вы можете использовать инструмент разбиения графа, такой как Metis, для кластеризации CNF предложения в независимые множества, которые не имеют общих переменных.
Если невозможно идентифицировать действительно отключенные кластеры, число "переменных связи" может быть достаточно маленьким, чтобы перечислить их значения. Такое перечисление в основном присваивает предварительное значение связующим переменным и исключает их для процесса поиска. Цена, которую нужно заплатить, заключается в том, что вы должны запустить поиск для каждой комбинации значений.
Современные SAT решатели, такие как Cryptominisat, Riss3g или Lingeling, применяют различные меры предварительной обработки, чтобы уменьшить масштаб проблемы. Однако 10000 переменных могут иметь допустимый размер, который можно решить без дополнительных действий.
Размер CNF сам по себе не является надежным показателем или сложностью проблемы. Кодирование Цейтина - это метод, часто используемый для уменьшения количества предложений в CNF.
Как рекомендовано в этом посте: Хорошая статья, которая содержит множество полезных ссылок на работу, касающуюся кодирования SAT, - "Успешные методы кодирования SAT". Автор Magnus Björk, 25 июля 2009 г.: http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf