Домашнее задание.
Обобщённое усиление выведенных из конфликтов ограничений - показывает, что отыскание ограничения конфликта минимального размера является, само по себе, NP-трудной задачей (то есть, даже проверка является NP-полной задачей).
Небольшое пояснение.
Для КНФ (коньюнктивной нормальной формы, то есть, Логического ИЛИ от Логических И от литералов) произвольное присваивание части переменных, совмещённое с выводом значений других переменных, может привести к противоречию. Обычно противоречие выглядит, как вывод одновременно значений истинно и ложно для какой-то переменной: при x=Истина (~x\/y)/\(~x\/~y) выводит и y=Истина и y=Ложь. Разрешение по переменной, для которой обнаружено противоречие, позволяет вывести новое ограничение, которое предотвратит вывод того же противоречия. Процесс разрешения это создание нового ограничения Логического ИЛИ, в которое входят все литералы ограничений, приведших к конфликту, но без литералов переменной конфликта: в нашем примере это, сперва, объединение ограничений (~x\/y\/~x\/~y), из которого исключили повторы и переменную y в любой полярности, то есть, (~x).
Выше продемонстрирован процесс "первого или ближайшего среза" - добавляем ограничение, что наиболее близко к конфликту. Мы можем идти по ациклическому графу вывода к нашему присваиванию, разрешая по любой переменной. В процессе мы можем вывести более короткое ограничение - чем короче ограничение, тем оно сильнее ограничивает пространство поиска.
Статья выше показывает, что поиск наиболее короткого ограничения это NP-сложная задача.
Однако, сравните с устранением избыточности поиска, где, в случае невозможности распространения значений переменных, выполняется решение много меньшей по размеру задачи булевской выполнимости для вычисления ограничения отсечения избыточности пространства поиска.
Теперь у меня вопрос: какого хрена?
Почему в одном случае мы будем решать NP-полную много более простую подзадачу, а в другом не будем? Почему мы не выполняем решение задачи усиления ограничения конфликта, несмотря на её выгодность? Почему, даже только что решив любую из задач из второй статьи, мы не выполняем поиск более сильного ограничения, нежели просто значения текущего присваивания?
Небольшое пояснение.
Для КНФ (коньюнктивной нормальной формы, то есть, Логического ИЛИ от Логических И от литералов) произвольное присваивание части переменных, совмещённое с выводом значений других переменных, может привести к противоречию. Обычно противоречие выглядит, как вывод одновременно значений истинно и ложно для какой-то переменной: при x=Истина (~x\/y)/\(~x\/~y) выводит и y=Истина и y=Ложь. Разрешение по переменной, для которой обнаружено противоречие, позволяет вывести новое ограничение, которое предотвратит вывод того же противоречия. Процесс разрешения это создание нового ограничения Логического ИЛИ, в которое входят все литералы ограничений, приведших к конфликту, но без литералов переменной конфликта: в нашем примере это, сперва, объединение ограничений (~x\/y\/~x\/~y), из которого исключили повторы и переменную y в любой полярности, то есть, (~x).
Выше продемонстрирован процесс "первого или ближайшего среза" - добавляем ограничение, что наиболее близко к конфликту. Мы можем идти по ациклическому графу вывода к нашему присваиванию, разрешая по любой переменной. В процессе мы можем вывести более короткое ограничение - чем короче ограничение, тем оно сильнее ограничивает пространство поиска.
Статья выше показывает, что поиск наиболее короткого ограничения это NP-сложная задача.
Однако, сравните с устранением избыточности поиска, где, в случае невозможности распространения значений переменных, выполняется решение много меньшей по размеру задачи булевской выполнимости для вычисления ограничения отсечения избыточности пространства поиска.
Теперь у меня вопрос: какого хрена?
Почему в одном случае мы будем решать NP-полную много более простую подзадачу, а в другом не будем? Почему мы не выполняем решение задачи усиления ограничения конфликта, несмотря на её выгодность? Почему, даже только что решив любую из задач из второй статьи, мы не выполняем поиск более сильного ограничения, нежели просто значения текущего присваивания?