ДПЛЛ(Т)
В информатике DPLL(T) представляет собой основу для определения выполнимости задач SMT . Алгоритм расширяет исходный SAT для решения алгоритм DPLL , добавляя возможность рассуждать о произвольной теории T . [ 1 ] [ 2 ] [ 3 ] На высоком уровне алгоритм работает путем преобразования задачи SMT в формулу SAT, в которой атомы заменяются логическими переменными. Алгоритм неоднократно находит удовлетворительную оценку для задачи SAT, консультируется с решателем теории , чтобы проверить согласованность с теорией, специфичной для предметной области, а затем (если обнаружено противоречие) уточняет формулу SAT с помощью этой информации. [ 4 ]
Многие современные решатели SMT, такие как Microsoft и Z3 теорема Prover CVC4 , используют DPLL(T) для реализации своих основных возможностей решения. [ 5 ] [ 6 ] [ 7 ]
Ссылки
[ редактировать ]- ^ Ганцингер, Харальд; Хаген, Джордж; Ньювенхейс, Роберт; Оливерас, Альберт; Тинелли, Чезаре (2004). «DPLL (T): процедуры быстрого принятия решений». В Алуре, Раджив; Пелед, Дорон А. (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 3114. Шпрингер Берлин Гейдельберг. стр. 175–188. дои : 10.1007/978-3-540-27813-9_14 . ISBN 9783540278139 .
- ^ Ньювенхейс, Роберт; Оливерас, Альберт; Тинелли, Чезаре (2006). «Решение теорий SAT и SAT по модулю: от абстрактной процедуры Дэвиса – Патнэма – Логемана – Лавленда к DPLL (T)». Дж. АКМ . 53 (6): 937–977. дои : 10.1145/1217856.1217859 . ISSN 0004-5411 . S2CID 14058631 .
- ^ Ньювенхейс, Роберт; Оливерас, Альберт (2005). «DPLL (T) с распространением исчерпывающей теории и ее применение к разностной логике». В Этессами – Куша; Раджамани, Шрирам К. (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 3576. Шпрингер Берлин Гейдельберг. стр. 321–334. дои : 10.1007/11513988_33 . ISBN 9783540316862 .
- ^ Рейнольдс, Эндрю (2015). «Теории выполнимости по модулю и DPLL (T)» (PDF) . Университет Айовы . Проверено 08 апреля 2019 г.
- ^ де Моура, Леонардо; Бьёрнер, Николай (2008). «Z3: эффективный решатель SMT». В Рамакришнане, Чехия; Рехоф, Якоб (ред.). Инструменты и алгоритмы построения и анализа систем . Конспекты лекций по информатике. Том. 4963. Шпрингер Берлин Гейдельберг. стр. 337–340. дои : 10.1007/978-3-540-78800-3_24 . ISBN 9783540788003 .
- ^ Лян, Тяньи; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк; Детерс, Морган (2014). «Решатель теории DPLL (T) для теории строк и регулярных выражений». В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 646–662. дои : 10.1007/978-3-319-08867-9_43 . ISBN 978-3-319-08867-9 .
- ^ Бруттометто, Роберто; Чиматти, Алессандро; Францен, Андерс; Гриджио, Альберто; Себастьяни, Роберто (2008). «Решатель MathSAT 4 SMT». В Гупте, Аарти ; Малик, Шарад (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том 5123. Springer Berlin Heidelberg. стр. 299–303. дои : 10.1007/978-3-540-70545-1_28 . ISBN 9783540705451 .