Алгоритм снижения выполнимости Java

Question

Существует ли какой-либо алгоритм для уменьшения задачи сат.,Не менее важно определить, не существует ли таких назначений, что подразумевает, что функция, выраженная формулой, одинаково ЛОЖЬ для всех возможных назначений переменных.В последнем случае мы бы сказали, что функция неудовлетворительная;в противном случае это выполнимо.Чтобы подчеркнуть бинарный характер этой проблемы, ее часто называют булевой или пропозициональной выполнимостью.Сокращение «SAT» также обычно используется для его обозначения с неявным пониманием того, что функция и все ее переменные имеют двоичное значение.

Я использовал генетические алгоритмы для решения этой проблемы, но этобудет проще, если уменьшится первым?

Answer 1

Взгляните на Диаграммы двоичных решений в уменьшенном порядке (ROBDD).Это обеспечивает способ сжатия логических выражений в сокращенную каноническую форму.Существует множество программ для выполнения сокращения BDD, ссылка на Википедию для ROBDD, приведенная выше, содержит хороший список внешних ссылок на другие соответствующие пакеты в нижней части статьи.

Answer 2

Вы, вероятно, могли бы выполнить поиск по дереву путей в глубину по формуле, чтобы определить «пути», т. Е. Для (ICanEat && (IHaveSandwich || IHaveBanana)), если «ICanEat» имеет значение false, значения в скобках не имеет значения и может быть проигнорировано. Итак, прямо здесь вы можете отбросить некоторые ребра и узлы.

И если во время генерации этого поиска в глубину текущий узел переходит в True, вы нашли свое решение.

Answer 3

Что вы имеете в виду под «сокращенным», точно?Я собираюсь предположить, что вы имеете в виду какую-то предварительную обработку заранее, чтобы сначала исключить или упростить некоторые переменные или предложения.

Все зависит от того, сколько работы вы хотите выполнить.Конечно, вы должны сделать распространение единицы , пока она не завершится.Есть и другие, более дорогие вещи, которые вы можете сделать.См. Раздел предварительной обработки на странице march_dl для некоторых примеров.