Проблема проверки выполнимости формул разрешимых теорий (обзор)
Vernadsky National Library of Ukraine
Переглянути архів Інформація| Поле | Співвідношення | |
| Title |
Проблема проверки выполнимости формул разрешимых теорий (обзор)
|
|
| Creator |
Скобелев, В.В.
|
|
| Description |
Данная работа посвящена анализу современного состояния исследований проблемы проверки выполнимости формул разрешимых теорий 1-го порядка на основе ѕленивого подходаї, т.е. на интеграции SAT-решателей с T -решателями. Охарактеризована структура SAT-решателя, построенного на основе управляющей конфликтами DPLL-процедуре. Рассмотрены основные понятия и принципы, используемые в процессе построения современных T -решателей. Изложение иллюстрируется на примере решателя, предназначенного для анализа выполнимости формул линейной целочисленной арифметики. Охарактеризованы методы организации взаимодействия SAT-решателей и T -решателей.
Дану статтю присв’ячено аналiзу сучасного стану дослiджень проблеми перевiрки здiйсненостi формул теорiй 1-го порядку на основi ѕледащого пiдходуї, тобто на iнтеграцiї SAT-вирiшувачiв з T -вирiшувачами. Охарактеризовано структуру SAT-вирiшувача, який побудовано на основi керуючою конфлiктами DPLL-процедури. Розглянуто основнi поняття та принципи, якi використуються при побудовi сучасних T -вирiшувачiв. Викладення iлюструється на прикладi вирiшувача, який призначено для перевiрки здiйсненостi формул лiнiйної арифметики цiлих чисел. Охарактеризовано методи iнтеграцiї SAT-вирiшувачiв з T -вирiшувачами. Given paper is devoted to analysis of the state of the art for investigations of the problem of checking for satisfiability of formulae in decidable first-order theories on the base of the lazy approach, i.e. on integration of SAT-solvers with T -solvers. The structure of SAT-solver designed on the base of conflict driven DPLL procedure is characterized. Basic notions and principles applied in the process of elaboration of modern T -solvers are considered. They are presented in detail for example of a solver intended for checking of satisfiability for formulae of linear integer arithmetic. Methods of integration of SAT-solvers with T -solvers are characterized. |
|
| Date |
2017-09-21T16:24:49Z
2017-09-21T16:24:49Z 2013 |
|
| Identifier |
Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос.
1683-4720 http://dspace.nbuv.gov.ua/handle/123456789/124170 512.552+519.95 |
|
| Language |
ru
|
|
| Relation |
Труды Института прикладной математики и механики
|
|
| Publisher |
Інститут прикладної математики і механіки НАН України
|
|