Главная » Просмотр файлов » Диссертация

Диссертация (1090534), страница 5

Файл №1090534 Диссертация (Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов) 5 страницаДиссертация (1090534) страница 52018-01-18СтудИзба
Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

Для проверки результата строится доказательствопротиворечия, описывающее последовательность шагов резолюций. В случаенеыполнимости поставленной задачи, последняя резолюция приведет к пустому21утверждени. Полученный ориентированный ациклический граф представляетсобой доказательство невыполнимости. Однако, данный подход повышаетпотребление вычислительных ресурсов в ходе решения задачи.Расширением алгоритмов SAT являются методы решения задачвыполнимости формул в теориях (англ. satisfiability modulo theories, SMT).Данный подход позволяет решать задачи выполнимости в терминах целых ивещественных чисел, теории списков и битовых векторов и др.

SMT теория можетвключать в себя произвольные переменные, а не только булевы. Предикатами жев этой теории может быть любое булевое выражение от этих переменных. SMTтеория предоставляет больше возможностей для моделирования, чем формулыSAT. Например, SMT-формула позволяет моделировать операции функциимодулей микропроцессора на уровне слов, а не на уровне битов.При разработке современного ПО большое внимание уделяетсятестированию и обеспечению корректности и надежности.

В работе [33]описывается программный комплекс KLEE, предоставляющий инструментысимвольного выполнения программы и автоматической генерации тестов.Программная система KLEE была использована для анализа 89 программ изпакета GNU Coreutils, которые установлены на миллионах компьютеров повсему миру и тщательно протестированы. Покртыие тестами составило более90% строчек кода, что существенно превышает покрытие тестами.

написаннымивручную. Также были проанализированы 75 программ пакета Busybox, для 31 изкоторых было достигнуто 100% покрытие кода. В общей сложности, при помощиKLEE были проанализированы 452 программы (более 430 тысяч строчек кода),в которых было обнаружено 56 критических ошибок. 3 из них не были найденына протяжении последних 15 лет.

KLEE использует SAT и SMT алгоритмы дляанализа исходных кодов ПО и генерации тестов.KLEE также используется в качестве инструмента для поиска ошибоки генерации тестов на базе документации (англ. Document-Assisted SymbolicExecution, DASE). Проект DASE. представленный в работе [34], используетметоды анализа естественного языка и эвристики для обработки документациик программной системе. В результате DASE автоматически выводит ограниченияна входные параметры ПО. Эта информация затем используетс для управленияпроцессом символьного выполнения, обращая больше внимания на семантическиважные участки кода.

При помощи DASE были проанализированы такие пакеты22программ, как foreutils, findutils, grep, binutils, elftoolchain. Было обнаружено12 критических, прежде неизвестных и не обнаруженных другими системамисимвольного выполнения, 6 из них подтверждены разработчиками. Степенипокрытия кода, условия и вызовов были улучшены на 14.2–120.3%, 2.3–167.7%и 16.9–135.2%, соответственно. 97.8-100% полученных ограничений корректны.В работе [35] рассматривается метод решения проблемы поиска пути всистмах с несколькими агентами.

Предметом исследования являются методыпоиска оптимальных решений, предотвращающих столкновения между агентами,в случае ненаправленных графов. Начальные и конечные позиции агентов могутразличаться. Существуют варианты формулировки этой задачи в виде SATпроблемы, минимизирующие число шагов, необходимых для достижения цели.В данной работе рассматривается метод минимизации числа шагов для каждогоагента, тем самым, выполняется поиск решения с наименьшей стоимостью.Экспериментальные результаты показывают, что данный подход обладаетпроизводительностью, сравнимой с лучшими известными реализациями.Для решения практических задач также большое значение имеют методырешения задачи MaxSAT.

В рамках этой задачи необходимо выполнить не всезаданные ограничения, а наибольшее их число. Такая формулировка позволяетрешать задачи оптимизации, возникающие в самых разных прикладных областях.Например, в работе [36] описаны различные прикладные задачи,возникающие при анализе данных, которые были успешно решены методомMaxSAT. Примерами таких задач являются минимизации весовой функции прикорреляционной кластеризации, построение вероятностной графической моделиминимального размера и анализ причинно-следственных связей. В результате,были предложены различные варианты трансляции этих прикладных задач кMaxSAT виду, поддержку вещественных коэффициентов при решении MaxSAT.В работе [37] рассматривается программная система автоматическогоуправления деловыми совещаниями и встречами.

В работе опиываютсяметоды трансляции исходной проблемы в задачу MaxSAT и использованныепсевдобулевы ограничения для оптимизации полученных графиков и расписаний.Экспериментальные результаты показывают, что предложенный алгоритмпревосходит предыдущие известные подходы.Практический интерес также представляет задача поиска не одноговыполняющего набора значений для заданной системы булевых выражений, а23всех.

Известные алгоритмы решения задачи выполнимости адресуют проблемупроверки выполнимости заданной формулы, а не поиска выполняющих наборов.Вместе с тем, активно развиваются параллельные методы решения задачивыполнимости. В работе [38] предлагается метод перечисления всех возможныхрешений для заданной формулы, в том числе и не в конъюнктивной нормальнойформе с использованием параллельных алгоритмов. Предложенный методпринимает в качестве входных данных выражение в алгебраической нормальнойформе. Алгоритм основан на идее представления выполняющих наборовзначений в виде полных множеств импликантов, которые выделены прифакторизации функции. Алгоритм эффективен при работе с функциями,содержащими малое число факторизованных переменных относительно ихобщего числа.

В таком случае объем вычислений полного множества импикантовминимален и с каждым шагом вычислений исходная формула продолжаетупрощаться. Данный алгоритм также может быть применен для поискаортогональных импликантов для функций в алгебраической нормальной форме.Весь процесс вычислений может быть разбит на небольшие независимые задачи,которые затем могут быть решены в распределенной среде. Предложенныйметод может быть использован при разработке эвристик для распределенныхалгоритмов решения задачи выполнимости булевых формул, которые используютбольшое число вычислительных ядер.При решении задач декларативного программирования нередко возникаетнеобходимость учета не только известной информации, но также и неизвестнойна данный момент.

В частности, на практике нередко возникают задачинемонотонной логики. Особенностью таких проблем является то, что свойствапроблемы, которые на текущий момент считаются истинными, могут бытьпризнаны ложными по мере поступления новой информации о задаче. Дляработы с такими проблемами значение имеет понятия “отрицания”. Одним изспособов работы с неизвестной информацией и отрицаниями является методпоиска стабильных моделей(англ.

answer set programming, ASP).Объемы информации и данных, которые собираются и обрабатываютсясовременными вычислительными системами неуклонно растут. Не являютсяисключением различные промышленные роботы. Возможность отделятькритичную для текущей работы информацию от не важной, является критичнойдля подобных систем. Возможность делать абстрактные выводы из полученных24данных пока еще недоступна вычислительным системам. Использование методовмашинного обучения для решения этой проблемы имеет свои ограничения, вчастности, роботизированная система сможет делать выводы только на базеуже известных (выученных) примерах. На практике, однако, не всегда естьвозможность обеспечить достаточно длительное и полное обучение программнойсистемы.

В работе [39] предлагается подход к решению данной проблемы наоснове ASP алгоритмов. В качестве примера рассматривается роботизированнаясистема, обслуживающая офисное помещение. Робот может делать выводыо важности или неважности полученных данных до выполнения каких-либодействий и операций.В статье [40] рассматриваются проблемы конфигурирования различныхпрограммных систем, в частности, продуктов компании Siemens.

Нередкопроблемы конфигурирования могут быть представлены в виде известныхвычислительных задач, таких как раскраска графа, задача об упаковке вконтейнеры и др., для решения которых существуют эффективные эвристики.Однако, нередко возникают проблемы, сочетающие в себе сразу несколькихтаких проблем. В данной работе рассматривается метод решения задачиконфигурирования с использованием декларативного программирования.Проблема сводится к задаче поиска стабильных моделей. Также в работерассматривается жадный алгоритм поиска решений, который улучшаетпроизводительность алгоритма ASP.Современная индустрия уделяет много внимания управлению кадрами.Оптимальное распределение задач и ресурсов имеет критическое влияниена успешность выполнения различных задач и позволяет избежать ситуацийнехватки ресурсов.

Характеристики

Список файлов диссертации

Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов
Документы
Свежие статьи
Популярно сейчас
А знаете ли Вы, что из года в год задания практически не меняются? Математика, преподаваемая в учебных заведениях, никак не менялась минимум 30 лет. Найдите нужный учебный материал на СтудИзбе!
Ответы на популярные вопросы
Да! Наши авторы собирают и выкладывают те работы, которые сдаются в Вашем учебном заведении ежегодно и уже проверены преподавателями.
Да! У нас любой человек может выложить любую учебную работу и зарабатывать на её продажах! Но каждый учебный материал публикуется только после тщательной проверки администрацией.
Вернём деньги! А если быть более точными, то автору даётся немного времени на исправление, а если не исправит или выйдет время, то вернём деньги в полном объёме!
Да! На равне с готовыми студенческими работами у нас продаются услуги. Цены на услуги видны сразу, то есть Вам нужно только указать параметры и сразу можно оплачивать.
Отзывы студентов
Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.
Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.
Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.
Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.
Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.
Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.
Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.
Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.
Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.
Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.
Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.
Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.
Популярные преподаватели
Добавляйте материалы
и зарабатывайте!
Продажи идут автоматически
6384
Авторов
на СтудИзбе
308
Средний доход
с одного платного файла
Обучение Подробнее