простой выпуск. У меня очень большой файл CNF, представляющий матрицу m x n. скажем> 10000 переменных со связанными терминами. Итак, на первом этапе я хочу разбить CNF-файл или даже лучше разбить матрицу на переменные 100 для параллельных решений. Есть ли какое-либо описание, какие правила применять?Сплит и/или разбиение большого файла CNF/Матрица
Вся помощь приветствуется.
С уважением Адриан
Вы можете использовать graph partitioning инструмент, как Metis сгруппировать CNF положения в независимые множества, которые не разделяют какие-либо переменные.
Если невозможно идентифицировать действительно отсоединенные кластеры, число «переменных ссылок» может быть достаточно маленьким, чтобы перечислять их значения. Такое перечисление в основном присваивает ориентировочное значение связующим переменным и исключает их для процесса поиска. Цена за оплату заключается в том, что вам нужно запустить поиск для каждой комбинации значений.
Современные решения SAT, такие как Cryptominisat, Riss3g или Lingeling, применяют различные меры предварительной обработки, чтобы уменьшить размер проблемы. Тем не менее, 10000 переменных могут быть допустимым размером, который можно решить без дополнительных шагов.
Размер CNF не является надежным индикатором или сложностью проблемы. Tseitin encoding - техника, часто используемая для уменьшения количества предложений в CNF.
В соответствии с рекомендациями this post: Хороший документ, который содержит много полезных ссылок на работы, касающиеся кодирования SAT является «Удачные SAT кодирования Techniques» Магнус Бьорк, 25 июля 2009: http://jsat.ewi.tudelft.nl/addendum/Bjork_encoding.pdf
спасибо, ВОЛЮ идти, хотя это –