Диссертация (1090534), страница 5
Текст из файла (страница 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.Современная индустрия уделяет много внимания управлению кадрами.Оптимальное распределение задач и ресурсов имеет критическое влияниена успешность выполнения различных задач и позволяет избежать ситуацийнехватки ресурсов.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
