Решение SAT с более чем 2 ^ 32 пунктами

Я пытаюсь решить большую формулу CNF, используя SAT solver. В формуле (в формате DIMACS) есть предложения 4,697,898,048 = 2^32 + 402,930,752, и все решатели SAT, которые я мог find испытывают проблемы с этим:

  • (P) lingeling сообщает, что "слишком много предложений" (т. е. больше предложений, чем указано в строке заголовка , Но это не так)
  • CryptoMiniSat4 и picosat утверждает, что в строке заголовка указано 402 930 752 предложения, что на 2 ^ 32 слишком мало
  • Глюкоза, кажется, анализирует 98 916 961 предложение, а затем сообщает, что формула была решена как UNSAT с использованием упрощения, но это вряд ли будет правильным (начальный сегмент формулы, такой короткий, скорее всего, будет SAT).

Кто-нибудь знает о решателе SAT, который может обрабатывать такие большие файлы? Или есть что-то вроде переключателя компилятора, который может обойти такое поведение? Я считаю, что все решатели скомпилированы для 64-битного Linux. (Я немного новичок, когда дело касается обработки таких больших чисел, извините.)


c integer-overflow sat sat-solvers
person Dominik Peters    schedule 17.09.2015    source источник
comment
Может быть, вы можете попробовать распределенный SAT-решатель.   -  person John Coleman    schedule 17.09.2015
comment
Это OSS? Вы можете изменить их, чтобы использовать целые числа 64b.   -  person Jeff Hammond    schedule 17.09.2015
comment
@Jeff: да, они все с открытым исходным кодом C или, может быть, C ++, не знаю, как отличить.   -  person Dominik Peters    schedule 17.09.2015
comment
Неважно. Целочисленные типы такие же :-)   -  person Jeff Hammond    schedule 17.09.2015
comment
Построение с 64-битными целыми числами вряд ли принесет много пользы в конечном итоге, потому что решатели на основе DPLL заведомо плохи на действительно больших экземплярах SAT. Стохастические решатели лучше, но даже среди тех, кого я никогда не слышал, чтобы найти формулу с более чем четырьмя миллиардами предложений.   -  person Kyle Jones    schedule 18.09.2015
comment
Можно ли разделить множество предложений на подмножества с непересекающимися переменными? Какое максимальное количество литералов в предложении?   -  person Axel Kemper    schedule 19.09.2015

Ответы (1)


arrow_upward
6
arrow_downward

Я разработчик CryptoMiniSat. В большинстве случаев, когда CNF настолько велика, проблема заключается не в решателе SAT, а в том, что перевод исходной проблемы в CNF был выполнен недостаточно тщательно. Я предполагаю, что вы не писали эту CNF вручную - у вас была проблема, которую вы перевели в CNF с помощью автоматизированного инструмента.

Акт перевода проблемы в CNF называется кодированием, и он имеет огромное количество литературы в академических кругах. Это отдельная тема или, что более уместно, целые темы сами по себе. Пожалуйста, ознакомьтесь с исследовательскими работами по программированию ограничений (CP), псевдобулевым ограничениям (PB), методам преобразования ANF в CNF (см. Семинары / конференции по криптовалюте) и кодированию электронных схем (найдите AIG, кодирование Цейтина и его варианты и посмотрите по ссылкам). Это большие темы, но есть много других. Взглянув на них, вы уменьшите вашу CNF как минимум на 3 порядка, а возможно, и больше.

person Mate Soos    schedule 17.09.2015
comment
Большое спасибо за ваш ответ. Для моей конкретной проблемы единственный способ уменьшить эквивалентное кодирование представляется мне путем получения относительно глубокого понимания нарушения симметрии, и я пессимистично отношусь к их существованию. Все более выразительные языки спецификации, которые вы упомянули, не позволили бы в этом случае более сжатое кодирование: моя проблема вполне естественно выражается в CNF, и, в частности, ни одна из переменных не является избыточной (вплоть до распространения единиц и потенциальных симметрий) - просто так получилось, что я ищу массивный объект. - person Dominik Peters; 17.09.2015
comment
К сожалению, я не уверен, что это естественно выражается в CNF, учитывая, что для его выражения требуется более 4 миллиардов пунктов. Вы, вероятно, могли бы выразить чип Apple A8 таким количеством пунктов, а это очень сложная система, на разработку которой потребовались десятки тысяч инженерных лет. Я предлагаю вам рассмотреть альтернативные способы выражения вашей проблемы. - person Mate Soos; 19.09.2015