SAT-решение системы одноразовых ограничений

Question

Я пытаюсь решить проблему SAT, которая состоит только из горячих ограничений. Прямо сейчас я использую горячую кодировку, предложенную Клессеном в гл. 4.2 из [1] и MiniSAT.

Интересно, есть ли лучший способ решения такой проблемы, например, класс решателей, который лучше подходит для такого рода задач по сравнению с решателями SAT на основе CNF. Я немного искал, но не могу найти много информации о SAT и ограничениях на одно горячее.

[1] Успешные методы кодирования SAT. Магнус Бджирк. 25 июля 2009

Answer 1

Решатели теоремы по модулю удовлетворительности часто являются хорошим выбором для выражения математических задач, которые в противном случае в конечном итоге были бы использованы в горячих кодировках CNF. Ключевым моментом является то, что только с помощью решателей на основе CNF и DPLL вы ограничены тем, что может эффективно обнаружить распространение единиц. На более высоком уровне абстракции существуют теории чисел и наборов, которые можно использовать для сокращения пространства поиска перед выборочным применением решателя SAT для более подходящих подзадач. Это то, что дает вам SMT, наряду с более выразительной силой и гораздо более приятным языком для выражения отношений.

Но если вы застряли с горячими ограничениями без ассоциированной математической задачи более высокого уровня, есть более эффективные способы кодирования одноразовых ограничений, которые требуют только линейного числа новых предложений для выражения отношения вместо обычного квадратичного увеличения. Увидеть

Эффективное кодирование CNF для выбора 1 из N объектов по Klieber и Kwon.