Выводимые ограничения
Предыдущие серии тут и по ссылкам оттуда.
Это про ограничения в алгоритмах поиска решения логической задачи. Conflict-driven clause learning, оно самое.
Я реализовал прямое использование ZDD для поиска наикратчайшего решения. Оно работает не так, чтобы плохо, я бы даже сказал, что хорошо, но может переполнить память, просто за счёт частого вызова объединения и разделения ("дай множества с наличием и отсутствием элемента"). Как ни крути, а квадрат.
Однако, мы можем строить ZDD непосредственно по хвостам ограничений, как Кнут как-то показывал в каком-то видео. Он строил все пути по шахматной доске, начиная от точки, куда надо придти. Построив все пути из точки А, он добавлял к ним путь из соседней с А точки Б. Такое не требует операции объединения.
Надо будет попробовать.
PS
Я даже видео то не смотрел, я просто идею запомнил. ;)
Это про ограничения в алгоритмах поиска решения логической задачи. Conflict-driven clause learning, оно самое.
Я реализовал прямое использование ZDD для поиска наикратчайшего решения. Оно работает не так, чтобы плохо, я бы даже сказал, что хорошо, но может переполнить память, просто за счёт частого вызова объединения и разделения ("дай множества с наличием и отсутствием элемента"). Как ни крути, а квадрат.
Однако, мы можем строить ZDD непосредственно по хвостам ограничений, как Кнут как-то показывал в каком-то видео. Он строил все пути по шахматной доске, начиная от точки, куда надо придти. Построив все пути из точки А, он добавлял к ним путь из соседней с А точки Б. Такое не требует операции объединения.
Надо будет попробовать.
PS
Я даже видео то не смотрел, я просто идею запомнил. ;)