Я использую решатель SAT для кодирования проблемы, и как часть экземпляра SAT, у меня есть логические переменные где предполагается, что именно одна из них должна быть истинной, а остальные должны быть ложным (Я иногда видел, что это описывается как «горячая» кодировка.)
Я хочу закодировать ограничение «ровно один из должно быть истинным» в SAT. Каков наилучший способ кодирования этого ограничения, чтобы заставить SAT-решатель работать максимально эффективно?
Я вижу много способов кодировать это ограничение:
Парные ограничения. Я мог бы добавить попарно ограничений для всех I , J , чтобы гарантировать , что не более одного х я верно, а затем добавить х 1 ∨ х 2 ∨ ⋯ ∨ х п , чтобы гарантировать , что по крайней мере один истинно.
Это добавляет предложений и никаких дополнительных логических переменных.
Бинарное кодирование. Я мог бы ввести новых логических переменных i 1 , i 2 , … , i lg n, чтобы представить (в двоичном виде) целое число i, такое что 1 ≤ i ≤ n (добавив несколько логических ограничений, чтобы убедиться, что i находится в желаемом диапазоне ). Затем я могу добавить ограничения, обеспечивающие, чтобы x i было деревом, а все остальные x j были ложными. Другими словами, для каждого j мы добавляем предложения, гарантирующие, что i = j .
Это добавляет предложений, и я не знаю, сколько дополнительных булевых переменных.
Подсчитайте количество истинных значений. Я мог бы реализовать дерево логических схем сумматора и потребовать, чтобы , рассматривая каждый x i как 0 или 1 вместо false или true, и использовать преобразование Цейтина для преобразования схемы в SAT статьи. Достаточно дерева половинных сумматоров: ограничьте выходной результат переноса каждого половинного сумматора равным 0, и ограничьте конечный выход конечного полумесяца в дереве равным 1. Дерево может быть выбрано, чтобы иметь любую форму ( сбалансированное бинарное дерево, или несбалансированное, или что угодно).
Это можно сделать в элементах и, таким образом, добавить Θ ( n ) предложений и Θ ( n ) новых логических переменных.
Особый случай такого подхода состоит в том, чтобы ввести логические переменные , с идеей , что у меня должно содержать значение х 1 ∨ х 2 ∨ ⋯ ∨ х I . Это намерение может быть обеспечено путем добавления положения у я ∨ ¬ х я , у я ∨ ¬ у я - 1 , а ¬ у я ∨ х я ∨ у я - (где мы рассматриваем y 0 как синоним false) дляi=1,…,n. Далее мы можем добавить ограничения¬ y i ∨¬ x i + 1 дляi=1,2,…,n-1. Это в основном эквивалентно преобразованию Цейтина дерева полусумметра, где дерево имеет максимально несбалансированную форму.
Сеть бабочек. Я мог бы построить сеть бабочки на биты, ограничивает п ввод -разрядного , чтобы быть 000 ⋯ 01 , ограничивает п выход -разрядного быть х 1 х - ⋯ х п , и рассматривать каждые 2-битовые бабочки ворот в качестве независимого ворот это либо меняет, либо не меняет входные данные с решением, которое делать на основе новой новой логической переменной, которая оставлена неограниченной. Затем я могу применить преобразование Цейтина для преобразования схемы в предложения SAT.
Это требует вентилей и, таким образом, добавляет Θ ( n lg n ) предложений и Θ ( n lg n ) новых логических переменных.
Есть ли другие методы, которые я пропустил? Какой я должен использовать? Кто-нибудь проверял это или пробовал их экспериментально, или у кого-нибудь есть опыт работы с любым из них? Является ли количество предложений и / или количество новых логических переменных хорошей метрикой для оценки влияния этого на производительность решателя SAT или, если нет, какую метрику вы бы использовали?
Я только что заметил, что в этом ответе есть некоторые ссылки на принудительное ограничение кардинальности для SAT, т. Е. Навязывание ограничения, согласно которому ровно из n переменных являются истинными. Итак, мой вопрос сводится к особому случаю, когда k = 1 . Возможно, литература по ограничениям мощности поможет пролить свет на мой вопрос.
Ответы:
Для особого случая k из n переменных true, где k = 1, существует кодирование переменной-коммандера, как описано в разделе Эффективное кодирование CNF для выбора объектов от 1 до N , авторы Klieber и Kwon. Упрощенно: разделите переменные на небольшие группы и добавьте предложения, которые приводят к тому, что состояние переменной commander подразумевает, что группа переменных является либо ложной, либо ложной. Затем рекурсивно примените тот же алгоритм к переменным коммандера. В конце процесса потребуйте, чтобы точно одна из нескольких переменных окончательного коммандера была истинной. Результатом является O (n) новых предложений и O (n) новых переменных.
Учитывая повсеместность литералов с двумя наблюдениями в решателях на основе DPLL, я думаю, что рост предложения O (n) является решающим преимуществом по сравнению со схемами кодирования, которые добавили бы больше предложений.
источник
В статье Магнуса Бьёрка описаны две техники, которые стоит попробовать.
Бумага
Магнус Бьорк. Успешные методы кодирования SAT . 25 июля 2009 г.
В следующей статье приведен подробный список кодировок для 1 изN а также К -снаружи-N с некоторой экспериментальной оценкой каждого из них. Выводы не совсем ясны (кодировка команд в своих экспериментах выглядит довольно неплохо).
Алан М. Фриш, Пол А. Джаннарос. SAT Кодировки ограничения At-Most-k: некоторые старые, некоторые новые, некоторые быстрые, некоторые медленные . ModRef 2010.
источник