Serguey Zefirov (thesz) wrote,
Serguey Zefirov
thesz

Полуночное размышление.

Я тут в твиттере распространялся про поиск наикратчайшего ограничения при поиске решения в алгоритме выведения ограничений из конфликтов (решение задачи логической разрешимости).

Важно найти наикратчайшее ограничение. "Сила" ограничения пропорциональна 2-длина ограничения.

При поиске ограничений мы 1) имеем дело с множеством "нарезаний" фронтов вывода и 2) нам надо применять алгоритмы разрешения (resolution) для уменьшения ограничений.

Первая неприятность приводит к экспоненциальному росту вариантов ограничений - выбор "включаем литерал или причины его вывода" применимо ко всем литералам некоторого вырезанного фронта.

Однако, у нас есть ZDD - диаграммы выбора с подавлением нулей. Они часто могут представить что-то экспоненциальное в квадратичном и даже линейном представлении. То есть, мы можем укладывать в ZDD нарезки фронтов, а уж она позаботиться об их сжатом представлении.

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

То есть, идея следующая: для всех фронтов строим ZDD со всеми возможными выводимыми ограничениями; к этой ZDD добавляем ограничения из нашей основной задачи, следя, чтобы это добавление упрощало; после чего считываем самый короткий путь по ZDD, можно не один.
Tags: cdcl, sat, логика
Subscribe

  • Вашему вниманию...

    ...предлагается взглянуть на DOP, применённый к HIGGS. DOP - это сокращение от "diagonal outer product". В выражении для аффинного преобразования…

  • Не йронки.

    https://github.com/thesz/higgs-logistic-regression Взял HIGGS dataset, натравил на него логистическое приближение (logistic regression) с…

  • Про word2vec.

    Word2vec это способ вычисления "вложений" (embeddings) для слов, основываясь на их окружении в тех местах, где они встречаются. Его можно считать…

  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments