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

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

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

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2013
Автор: Скобелев, В.В.
Мова:Russian
Опубліковано: Інститут прикладної математики і механіки НАН України 2013
Назва видання:Труды Института прикладной математики и механики
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/124170
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-124170
record_format dspace
spelling irk-123456789-1241702017-09-22T03:02:45Z Проблема проверки выполнимости формул разрешимых теорий (обзор) Скобелев, В.В. Данная работа посвящена анализу современного состояния исследований проблемы проверки выполнимости формул разрешимых теорий 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. 2013 Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос. 1683-4720 http://dspace.nbuv.gov.ua/handle/123456789/124170 512.552+519.95 ru Труды Института прикладной математики и механики Інститут прикладної математики і механіки НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Russian
description Данная работа посвящена анализу современного состояния исследований проблемы проверки выполнимости формул разрешимых теорий 1-го порядка на основе ѕленивого подходаї, т.е. на интеграции SAT-решателей с T -решателями. Охарактеризована структура SAT-решателя, построенного на основе управляющей конфликтами DPLL-процедуре. Рассмотрены основные понятия и принципы, используемые в процессе построения современных T -решателей. Изложение иллюстрируется на примере решателя, предназначенного для анализа выполнимости формул линейной целочисленной арифметики. Охарактеризованы методы организации взаимодействия SAT-решателей и T -решателей.
author Скобелев, В.В.
spellingShingle Скобелев, В.В.
Проблема проверки выполнимости формул разрешимых теорий (обзор)
Труды Института прикладной математики и механики
author_facet Скобелев, В.В.
author_sort Скобелев, В.В.
title Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_short Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_full Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_fullStr Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_full_unstemmed Проблема проверки выполнимости формул разрешимых теорий (обзор)
title_sort проблема проверки выполнимости формул разрешимых теорий (обзор)
publisher Інститут прикладної математики і механіки НАН України
publishDate 2013
url http://dspace.nbuv.gov.ua/handle/123456789/124170
citation_txt Проблема проверки выполнимости формул разрешимых теорий (обзор) / В.В. Скобелев // Труды Института прикладной математики и механики НАН Украины. — Донецьк: ІПММ НАН України, 2013. — Т. 26. — С. 205-221. — Бібліогр.: 94 назв. — рос.
series Труды Института прикладной математики и механики
work_keys_str_mv AT skobelevvv problemaproverkivypolnimostiformulrazrešimyhteorijobzor
first_indexed 2023-10-18T20:45:48Z
last_indexed 2023-10-18T20:45:48Z
_version_ 1796151045741608960

Схожі ресурси