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

Концепция в задаче булевой выполнимости

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

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

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

Минимальное невыполнимое ядро содержит наименьшее количество исходных предложений, необходимых для того, чтобы быть невыполнимым. Неизвестны практические алгоритмы для вычисления минимального невыполнимого ядра, ^[3] а вычисление минимального невыполнимого ядра входной формулы в конъюнктивной нормальной форме является -полной проблемой. ^[4] Обратите внимание на терминологию: в то время как минимальное невыполнимое ядро было локальной проблемой с простым решением, минимальное невыполнимое ядро является глобальной проблемой без известного простого решения. $\Сигма _{2}^{\mathsf {P}}$

Ссылки

^ Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). "Масштабируемый алгоритм для извлечения минимального невыполнимого ядра" (PDF) . В Biere, A.; Gomes, CP (ред.). Теория и применение тестирования выполнимости — SAT 2006 . Конспект лекций по информатике. Том 4121. Springer. стр. 36–41 . arXiv : cs/0605085 . CiteSeerX 10.1.1.101.5209 . doi :10.1007/11814948_5. ISBN 978-3-540-37207-3. S2CID 2845982.
^ Szeider, Stefan (декабрь 2004 г.). «Минимальные невыполнимые формулы с ограниченной разностью переменных в предложениях являются фиксированно-параметрическими». Журнал компьютерных и системных наук . 69 (4): 656– 674. CiteSeerX 10.1.1.634.5311 . doi :10.1016/j.jcss.2004.04.009.
^ Лиффитон, М. Х.; Сакаллах, К. А. (2008). «Алгоритмы для вычисления минимальных невыполнимых подмножеств ограничений» (PDF) . J Autom Reason . 40 : 1–33 . CiteSeerX 10.1.1.79.1304 . doi :10.1007/s10817-007-9084-z. S2CID 11106131.
^ "Сложность вычисления минимального невыполнимого ядра". Theoretical Computer Science Stack Exchange . Получено 2024-09-24 .

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

[1] Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). "Масштабируемый алгоритм для извлечения минимального невыполнимого ядра" (PDF) . В Biere, A.; Gomes, CP (ред.). Теория и применение тестирования выполнимости — SAT 2006 . Конспект лекций по информатике. Том 4121. Springer. стр. 36–41 . arXiv : cs/0605085 . CiteSeerX 10.1.1.101.5209 . doi :10.1007/11814948_5. ISBN 978-3-540-37207-3. S2CID 2845982.

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

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

[4] "Сложность вычисления минимального невыполнимого ядра". Theoretical Computer Science Stack Exchange . Получено 2024-09-24 .