Проблема проверки выполнимости формул разрешимых теорий (обзор)
Данная работа посвящена анализу современного состояния исследований проблемы проверки выполнимости формул разрешимых теорий 1-го порядка на основе ѕленивого подходаї, т.е. на интеграции SAT-решателей с T -решателями. Охарактеризована структура SAT-решателя, построенного на основе управляющей конфлик...
Saved in:
| Published in: | Труды Института прикладной математики и механики |
|---|---|
| Date: | 2013 |
| Main Author: | |
| Language: | Russian |
| Published: |
Інститут прикладної математики і механіки НАН України
2013
|
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/124170 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862667716059463680 |
|---|---|
| author | Скобелев, В.В. |
| author_facet | Скобелев, В.В. |
| citation_txt | Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос. |
| collection | DSpace DC |
| container_title | Труды Института прикладной математики и механики |
| 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.
|
| first_indexed | 2025-12-07T15:22:50Z |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-124170 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1683-4720 |
| language | Russian |
| last_indexed | 2025-12-07T15:22:50Z |
| publishDate | 2013 |
| publisher | Інститут прикладної математики і механіки НАН України |
| record_format | dspace |
| spelling | Скобелев, В.В. 2017-09-21T16:24:49Z 2017-09-21T16:24:49Z 2013 Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос. 1683-4720 https://nasplib.isofts.kiev.ua/handle/123456789/124170 512.552+519.95 Данная работа посвящена анализу современного состояния исследований проблемы проверки выполнимости формул разрешимых теорий 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. ru Інститут прикладної математики і механіки НАН України Труды Института прикладной математики и механики Проблема проверки выполнимости формул разрешимых теорий (обзор) Проблема перевiрки здiйсненостi формул розв’язних теорiй (огляд) Problem of checking for satisfiability of formulae of decidable theories (survey) published earlier |
| spellingShingle | Проблема проверки выполнимости формул разрешимых теорий (обзор) Скобелев, В.В. |
| title | Проблема проверки выполнимости формул разрешимых теорий (обзор) |
| title_alt | Проблема перевiрки здiйсненостi формул розв’язних теорiй (огляд) Problem of checking for satisfiability of formulae of decidable theories (survey) |
| title_full | Проблема проверки выполнимости формул разрешимых теорий (обзор) |
| title_fullStr | Проблема проверки выполнимости формул разрешимых теорий (обзор) |
| title_full_unstemmed | Проблема проверки выполнимости формул разрешимых теорий (обзор) |
| title_short | Проблема проверки выполнимости формул разрешимых теорий (обзор) |
| title_sort | проблема проверки выполнимости формул разрешимых теорий (обзор) |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/124170 |
| work_keys_str_mv | AT skobelevvv problemaproverkivypolnimostiformulrazrešimyhteoriiobzor AT skobelevvv problemaperevirkizdiisnenostiformulrozvâznihteoriioglâd AT skobelevvv problemofcheckingforsatisfiabilityofformulaeofdecidabletheoriessurvey |