Проблема проверки выполнимости формул разрешимых теорий (обзор)

Проблема проверки выполнимости формул разрешимых теорий (обзор)

Данная работа посвящена анализу современного состояния исследований проблемы проверки выполнимости формул разрешимых теорий 1-го порядка на основе ѕленивого подходаї, т.е. на интеграции SAT-решателей с T -решателями. Охарактеризована структура SAT-решателя, построенного на основе управляющей конфлик...

Ausführliche Beschreibung

Gespeichert in:
Bibliographische Detailangaben
Veröffentlicht in:Труды Института прикладной математики и механики
Datum:2013
1. Verfasser: Скобелев, В.В.
Sprache:Russian
Veröffentlicht: Інститут прикладної математики і механіки НАН України 2013
Online Zugang:https://nasplib.isofts.kiev.ua/handle/123456789/124170
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-124170
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
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Проблема проверки выполнимости формул разрешимых теорий (обзор)
spellingShingle Проблема проверки выполнимости формул разрешимых теорий (обзор)
Скобелев, В.В.
title_short Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_full Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_fullStr Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_full_unstemmed Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_sort проблема проверки выполнимости формул разрешимых теорий (обзор)
author Скобелев, В.В.
author_facet Скобелев, В.В.
publishDate 2013
language Russian
container_title Труды Института прикладной математики и механики
publisher Інститут прикладної математики і механіки НАН України
title_alt Проблема перевiрки здiйсненостi формул розв’язних теорiй (огляд)
Problem of checking for satisfiability of formulae of decidable theories (survey)
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.
issn 1683-4720
url https://nasplib.isofts.kiev.ua/handle/123456789/124170
citation_txt Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос.
work_keys_str_mv AT skobelevvv problemaproverkivypolnimostiformulrazrešimyhteoriiobzor
AT skobelevvv problemaperevirkizdiisnenostiformulrozvâznihteoriioglâd
AT skobelevvv problemofcheckingforsatisfiabilityofformulaeofdecidabletheoriessurvey
first_indexed 2025-12-07T15:22:50Z
last_indexed 2025-12-07T15:22:50Z
_version_ 1850863486510301184

Ähnliche Einträge