Продолжение про поиск наименьшего ограничения.
Начало про общую идею, необходимые структуры данных и тп.
Надо рассмотреть взаимодействие между возможностями уменьшения ограничений.
Это довольно просто.
Уменьшение ограничений выполняется через разрешение (resolution). Если у нас есть ограничение a∨b∨c и ограничение a∨!c, то мы можем разрешить эти два ограничения по переменной c и получить вместо первого ограничения в три переменных новое, в две переменных a∨b.
Разрешения могут мешать друг другу. Допустим, мы пытаемся уменьшить ограничение a∨b∨c∨d∨e∨f и у нас есть два кандидата на разрешение: a∨!b и b∨!c. Если мы применим первый, то второй применить не получится. Наоборот, в этом примере, можно, но так же можно придумать случай, когда только одно разрешение возможно.
Получается, что нам надо решить задачу перебора: какие ограничения-кандидаты мы можем применить для уменьшения нашего нового ограничения?
Упрощение этой задачи состоит в том, что ограничения-кандидаты можно разделить на пересекающиеся и не пересекающиеся. Если у нас только не пересекающиеся, то перебора нет - накатывай и радуйся. Если есть пересечение, то мы, о радость, можем формировать большее ограничение-кандидат, выполняя разрешение поверх кандидатов! После чего использовать упрощения, начиная с самого большого.
Вот эта вот радость выше, она всё ещё NP-полна, фактически, это алгоритм Davis-Putnam (от него отказались слишком рано, некоторые могут подумать): мы выбираем переменную и разрешаем по ней все ограничения, устраняя её из задачи. У нас, правда, большинство ограничений пересекаться не будет и те, что будут, будут принадлежать много более узкому подмножеству всех ограничений задачи.
Это как с умножением матриц: разбив матрицы на половинки, мы можем получить более простую задачу. Так и здесь - упрощение новых ограничений может быть выполнено только с определёнными ограничениями на значения переменных в них, не со всеми ограничениями задачи.
Вспоминая SaDiCal с его "решением много более простой задачи в случае останова вывода значений переменных", мы получаем много более простую задачу и здесь.
Надо рассмотреть взаимодействие между возможностями уменьшения ограничений.
Это довольно просто.
Уменьшение ограничений выполняется через разрешение (resolution). Если у нас есть ограничение a∨b∨c и ограничение a∨!c, то мы можем разрешить эти два ограничения по переменной c и получить вместо первого ограничения в три переменных новое, в две переменных a∨b.
Разрешения могут мешать друг другу. Допустим, мы пытаемся уменьшить ограничение a∨b∨c∨d∨e∨f и у нас есть два кандидата на разрешение: a∨!b и b∨!c. Если мы применим первый, то второй применить не получится. Наоборот, в этом примере, можно, но так же можно придумать случай, когда только одно разрешение возможно.
Получается, что нам надо решить задачу перебора: какие ограничения-кандидаты мы можем применить для уменьшения нашего нового ограничения?
Упрощение этой задачи состоит в том, что ограничения-кандидаты можно разделить на пересекающиеся и не пересекающиеся. Если у нас только не пересекающиеся, то перебора нет - накатывай и радуйся. Если есть пересечение, то мы, о радость, можем формировать большее ограничение-кандидат, выполняя разрешение поверх кандидатов! После чего использовать упрощения, начиная с самого большого.
Вот эта вот радость выше, она всё ещё NP-полна, фактически, это алгоритм Davis-Putnam (от него отказались слишком рано, некоторые могут подумать): мы выбираем переменную и разрешаем по ней все ограничения, устраняя её из задачи. У нас, правда, большинство ограничений пересекаться не будет и те, что будут, будут принадлежать много более узкому подмножеству всех ограничений задачи.
Это как с умножением матриц: разбив матрицы на половинки, мы можем получить более простую задачу. Так и здесь - упрощение новых ограничений может быть выполнено только с определёнными ограничениями на значения переменных в них, не со всеми ограничениями задачи.
Вспоминая SaDiCal с его "решением много более простой задачи в случае останова вывода значений переменных", мы получаем много более простую задачу и здесь.