Неудовлетворительное ядро

В математической логике , учитывая невыполнимую булеву формулу высказывания в конъюнктивной нормальной форме , подмножество предложений, соединение которых все еще невыполнимо, называется невыполнимым ядром исходной формулы.

Многие решатели SAT могут создать график разрешения , который доказывает невыполнимость исходной задачи. Это можно проанализировать, чтобы получить меньшее невыполнимое ядро.

Невыполнимое ядро называется минимальным невыполнимым ядром , если каждое его правильное подмножество (допускающее удаление любого произвольного предложения или предложений) является выполнимым. Таким образом, такое ядро является локальным минимумом , хотя и не обязательно глобальным. Существует несколько практических методов вычисления минимальных невыполнимых ядер. ^[1]^[2]

Минимальное невыполнимое ядро содержит наименьшее количество исходных предложений, которые должны оставаться невыполнимыми. Практические алгоритмы вычисления минимального ядра неизвестны. ^[3] Обратите внимание на терминологию: в то время как минимальное невыполнимое ядро было локальной проблемой с простым решением, минимальное невыполнимое ядро — это глобальная проблема, простого решения которой не известно.

Ссылки

^ Дершовиц, Н.; Ханна, З.; Надель, А. (2006). «Масштабируемый алгоритм минимального невыполнимого извлечения ядра» (PDF) . В Бьере, А.; Гомес, К.П. (ред.). Теория и применение тестирования выполнимости — SAT 2006 . Конспекты лекций по информатике. Том. 4121. Спрингер. стр. 36–41. arXiv : cs/0605085 . CiteSeerX 10.1.1.101.5209 . дои : 10.1007/11814948_5 . ISBN 978-3-540-37207-3 . S2CID 2845982 .
^ Зейдер, Стефан (декабрь 2004 г.). «Минимальные невыполнимые формулы с ограниченной разностью переменных предложения являются управляемыми с фиксированными параметрами». Журнал компьютерных и системных наук . 69 (4): 656–674. CiteSeerX 10.1.1.634.5311 . дои : 10.1016/j.jcss.2004.04.009 .
^ Лиффитон, Миннесота; Сакалла, Калифорния (2008). «Алгоритмы вычисления минимальных невыполнимых подмножеств ограничений» (PDF) . J Автоматический разум . 40 : 1–33. CiteSeerX 10.1.1.79.1304 . дои : 10.1007/s10817-007-9084-z . S2CID 11106131 .

Эта логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

[1] Дершовиц, Н.; Ханна, З.; Надель, А. (2006). «Масштабируемый алгоритм минимального невыполнимого извлечения ядра» (PDF) . В Бьере, А.; Гомес, К.П. (ред.). Теория и применение тестирования выполнимости — SAT 2006 . Конспекты лекций по информатике. Том. 4121. Спрингер. стр. 36–41. arXiv : cs/0605085 . CiteSeerX 10.1.1.101.5209 . дои : 10.1007/11814948_5 . ISBN 978-3-540-37207-3 . S2CID 2845982 .

[2] Зейдер, Стефан (декабрь 2004 г.). «Минимальные невыполнимые формулы с ограниченной разностью переменных предложения являются управляемыми с фиксированными параметрами». Журнал компьютерных и системных наук . 69 (4): 656–674. CiteSeerX 10.1.1.634.5311 . дои : 10.1016/j.jcss.2004.04.009 .

[3] Лиффитон, Миннесота; Сакалла, Калифорния (2008). «Алгоритмы вычисления минимальных невыполнимых подмножеств ограничений» (PDF) . J Автоматический разум . 40 : 1–33. CiteSeerX 10.1.1.79.1304 . дои : 10.1007/s10817-007-9084-z . S2CID 11106131 .

[1]

[2]

[3]