Полуночное размышление.
Я тут в твиттере распространялся про поиск наикратчайшего ограничения при поиске решения в алгоритме выведения ограничений из конфликтов (решение задачи логической разрешимости).
Важно найти наикратчайшее ограничение. "Сила" ограничения пропорциональна 2-длина ограничения.
При поиске ограничений мы 1) имеем дело с множеством "нарезаний" фронтов вывода и 2) нам надо применять алгоритмы разрешения (resolution) для уменьшения ограничений.
Первая неприятность приводит к экспоненциальному росту вариантов ограничений - выбор "включаем литерал или причины его вывода" применимо ко всем литералам некоторого вырезанного фронта.
Однако, у нас есть ZDD - диаграммы выбора с подавлением нулей. Они часто могут представить что-то экспоненциальное в квадратичном и даже линейном представлении. То есть, мы можем укладывать в ZDD нарезки фронтов, а уж она позаботиться об их сжатом представлении.
Ответив на первую неприятность, мы также может разобраться и со второй. Структуры данных типа BDD/ZDD могут успешно применяться для выполнения разрешения (resolution) по переменной (статья содержит неточности, есть доклад на эту тему, там правильные формулы, но я уже устал). Причём там вообще волшебно получается - добавляя ограничение к набору ограничений, мы одновременно получаем упрощение, если это возможно.
То есть, идея следующая: для всех фронтов строим ZDD со всеми возможными выводимыми ограничениями; к этой ZDD добавляем ограничения из нашей основной задачи, следя, чтобы это добавление упрощало; после чего считываем самый короткий путь по ZDD, можно не один.
Важно найти наикратчайшее ограничение. "Сила" ограничения пропорциональна 2-длина ограничения.
При поиске ограничений мы 1) имеем дело с множеством "нарезаний" фронтов вывода и 2) нам надо применять алгоритмы разрешения (resolution) для уменьшения ограничений.
Первая неприятность приводит к экспоненциальному росту вариантов ограничений - выбор "включаем литерал или причины его вывода" применимо ко всем литералам некоторого вырезанного фронта.
Однако, у нас есть ZDD - диаграммы выбора с подавлением нулей. Они часто могут представить что-то экспоненциальное в квадратичном и даже линейном представлении. То есть, мы можем укладывать в ZDD нарезки фронтов, а уж она позаботиться об их сжатом представлении.
Ответив на первую неприятность, мы также может разобраться и со второй. Структуры данных типа BDD/ZDD могут успешно применяться для выполнения разрешения (resolution) по переменной (статья содержит неточности, есть доклад на эту тему, там правильные формулы, но я уже устал). Причём там вообще волшебно получается - добавляя ограничение к набору ограничений, мы одновременно получаем упрощение, если это возможно.
То есть, идея следующая: для всех фронтов строим ZDD со всеми возможными выводимыми ограничениями; к этой ZDD добавляем ограничения из нашей основной задачи, следя, чтобы это добавление упрощало; после чего считываем самый короткий путь по ZDD, можно не один.