Автореферат (1090533), страница 3
Текст из файла (страница 3)
В рамках данного подхода описание задачи и ее решения представляются в видетеоремы, которая затем доказывается. В случае, когда полученная теорема несодержит противоречий и может быть доказана; результат такого доказательства соответствует решению исходной задачи. Алгоритмы, решающие задачувыполнимости подобных теорем, называются разрешающими процедурами.Подход, основанный на использовании этих процедур, активно используетсяпри решении задач верификации, автоматического синтеза тестов, при решении задач планирования и составления расписаний, при решении оптимизационных задач.Результатом активных исследований в области решения задачи выполнимости булевых формул ВЫП, известной в англоязычной литературе подназванием SAT, которая принадлежит классу NP–полных, является семейство эффективных алгоритмов, известных под названием SAT.
Для ускоренияпроцедуры поиска используется такие подходы, как распространение констант, правило резолюций, обучение с конфликтами, нехронологический поиск с возвратами.Дальнейшее развитие этих алгоритмов опирается на использованиеразличных эвристик, политик сброса, использование кэшей. Развитие методов решения задачи SAT позволило также и поиск методов решения болеесложных задач. Например, практический интерес представляет задачаMaxSAT — процедура поиска такого решения заданной теоремы, при котором могут быть удовлетворены не все заданные ограничения, а максимальновозможное их число.
Ведутся исследования в области решения задач выполнимости квантифицированных булевых формул (англ. quantified booleanformulas, QBF). В ряде практических задач необходимо найти не одно решение заданной формулы, а все возможные, или необходимо оценить число таких решений. Для этого используются алгоритмы семейства Sharp–SAT(#SAT).Формальные методы позволяют по заданной спецификации получитьмодель (решение), удовлетворяющей всем заданным ограничениям.
В практических задачах зачастую интерес представляют не только сами модели, нои отношения между ними. Теория графов предоставляет удобный формализмдля описания связей между объектами. Практический интерес представляетзадача разбиения графа — выделение подграфов по определенным правилам.
Примерами таких разбиений может быть задача раскраски графа, поисккомпонентов связности и клик (полных подграфов). Многие актуальные задачи могут быть сведены к процедуре поиска максимальной клики графа илиперечислению всех максимальных клик. Подобное разбиение исходного графа описывает попарные отношения между его элементами.11Описание задач, представленное в виде логических выражений, можетсодержать избыточные переменные и выражения. Эти данные не сообщаютновой информации о свойствах и параметрах решения, однако, увеличиваютобъемы вычислительных ресурсов, необходимых для работы с таким представлением.
Для сокращения потребления этих ресурсов могут быть использованы методы минимизации логических функций. Целью работы данныхалгоритмов является поиск минимального описания исходной функции.Третья глава посвящена разработке вычислительного комплекса автоматического вывода правил на границах структурных компонентов на базетехнологии декларативного программирования. Описывается модель данных,способ представления и манипуляций над правилами проектирования. Вводится понятие трассировочной сетки, в узлах которой могут размещатьсяэлементы топологии — элементы металлов, переходные отверстия и др. Водном узле могут быть размещены объекты разных типов.Основными этапами реализации предлагаемого алгоритма являются:1.
Построение окна, достаточно большого, чтобы вместить все исследуемые правила проектирования. В окне создаются границы ячеек, как вертикальные, так и горизонтальные.2. Формирование списка правил проектирования, зона влияния которыхвыходит за границы стандартных ячеек.3. Перечисление таких топологий внутри полученного окна, которые несодержат нарушений правил проектирования.4. Группировка разрешенных топологий в такие множества, что любаяпара топологий, принадлежащих одному множеству, не образует нарушений.5. Построение правил проектирования на границах ячеек, соответствующих каждой группе топологий.Блок–схема алгоритма представлена на Рисунке 2.
В рамках диссертационной работы был реализован программный модуль для вывода дополнительных правил на границах ячеек.Рис. 2. Этапы алгоритма вывода дополнительных правил проектирования награницах стандартных ячеек12В качестве модели описания правил проектирования в диссертационной работе используется подход, представленный в работе (Suto, 2012). В основе предложенного метода лежит использование трассировочных сеток дляописания топологий. В узлах трассировочной сетки размещаются дискретныеэлементы топологии фиксированного размера — элементы металлов и переходные отверстия.
Правила проектирования представляются в виде выражений логики высказываний над дискретными элементами топологии. Примертопологии приведен на Рисунке 3. Трассировочная сетка обозначена тонкимичерными линиями, объектыисоответствуют переходным отверстиям.В рассматриваемом примере данная топология запрещена правилами проектирования.Рис.
3. Пример представления топологии на трассировочной сеткеВ диссертационной работе был реализована процедура, представляющая входные правила проектирования в виде логических выражений. Каждому объекту топологии сопоставляется булева переменная: ее значение равно Истина, когда дискретный элемент топологии присутствует в заданнойпозиции; если ее значение Ложь, то объект отсутствует.
Логические выражения, описывающие правила проектирования, возвращают значение Истина, если топология содержит нарушения заданных ограничений. Правило, запрещающее топологию, представленную на Рисунке 3, может быть записанов виде выражения логики высказываний:(1)В случае, если оба объектаипредставлены в топологии, формула(1) возвращает значение Истина. Данное правило, таким образом, можетбыть представлено в виде логического вентиля И.В диссертационной работе для поиска разрешенных топологий используются алгоритмы SAT. Специальные программы решатели (англ. SAT solvers), реализующие данный алгоритм, в качестве входных данных принимаютформулы в конъюнктивной нормальной форме (КНФ). Результатом работырешателя является такой набор значений входных параметров, для которогозаданная КНФ возвращает значение Истина.
Любое логическое выражениеможет быть представлено в виде КНФ. Для подобного преобразования в об-13щем случае может потребоваться 2n дополнительных конъюнктов, где n —число переменных.В диссертационной работе реализован метод трансляции Цейтина с использованием вспомогательных переменных (Tseitin, 1983). В данной работевспомогательная переменнаясоответствует выходу логического вентиля.Несмотря на то, что полученная формула содержит больше переменных, онаможет быть удовлетворена теми же значениями входных параметров, что иисходная. Таким образом, полученная КНФ формула возвращает значениеИстина тогда и только тогда, когда удовлетворено исходное выражение логики высказываний.
Длина итоговой КНФ формулы растет линейно от числапеременных.Рассмотрим следующее выражение:(2)Таблица истинности, описывающая формулу (2) представлена в Таблице 1. Наборы входных значений, для которых (2) возвращает значение Истина, соответствует таблице истинности формулы (1). Наборы входных значений, для которых значение переменной out равно Ложь, описывают топологии, не содержащие нарушений правил проектирования. В Таблице 1 такиенаборы отмечены жирным.Функция, описанная выделенными строками таблицы истинности, может быть получена из формулы (2) добавлением дизъюнкта единичной длины. Полученное выражение возвращает значение Истина тогда и только тогда, когда набор входных значений соответствует разрешенной топологии:(3)Таблица 1Таблица истинности формулы (2)10101001100011111010100101110000Выражение (3) может быть выполнено только при значении, равном Истина.
Данное наблюдение позволяет упростить полученную формулу:КНФ формула, описывающая разрешенные топологии с учетом всехзаданных ограничений, должна возвращать значение Истина для наборов14значений, удовлетворяющих всем заданными ограничениям. Такая формулапредставляет собой конъюнкцию всех выражений, соответствующих правилам проектирования:(4)На следующем этапе реализовано построение окна, достаточно большого, чтобы вместить входные правила проектирования. Высота окна зафиксирована и равна высоте ряда стандартных ячеек. Ширина окна определяетсяразмерами исследуемых правил проектирования.В диссертационной работе границы ячеек интерпретируются как осисимметрий, как в горизонтальном, так и в вертикальном направлении.
Инымисловами, если объект запрещен во всех топологиях, соответствующие емуобъекты справа и снизу от границ ячеек также должны быть запрещены. Еслиобъект может появляться в топологиях, то соответствующие ему объектытакже разрешены. Таким образом, к формуле (4) необходимо добавить выражение, которое возвращает значение Истина в случае, когда входящие в негопеременные имеют одинаковое значение и возвращает Ложь во всех другихслучаях:(5)Выражениедобавляет ограничение на равенство пары входных значений. В силу ограниченности объема автореферата далее по тексту ограничениеопускается, но должно быть учтено при реализации обсуждаемыхалгоритмов.Для поиска таких наборов входных параметров, при которых формула(5) удовлетворена, в диссертационной работе был реализован алгоритм, основанный на теории выполнимости булевых формул (англ.
satisfiability,SAT). На базе алгоритма SAT можно построить метод перечисления всехудовлетворяющих наборов переменных, известный под названием AllSAT.Отличительной особенностью алгоритмов SAT и AllSAT является точность— они гарантированно находят все возможные решения.Результатом работы алгоритма AllSAT является формула в дизъюнктивной нормальной форме (ДНФ). Каждая конъюнкция в ней соответствуетодной из возможных разрешенных топологий:(6)15а)б)в)г)д)Рис. 4.
Множество разрешенных топологий, полученных методомAllSATКаждый полученный дизъюнкт обладает одним свойством — соответствующая топология, будучи поставленная встык к самой себе, образует также разрешенную топологию (Рисунок 5). Разные пары полученных топологий могут образовывать как разрешенные, так и запрещенные комбинации(Рисунок 6).Рис. 5. Примеры разрешенных топологий, составленных из одинаковыхэлементова)б)Рис. 6. Примеры топологий, составленных из различных составныхчастей. Топология (а) разрешена, (б) запрещенаВ диссертационной работе был реализован поиск таких групп топологий, что любые две топологии, принадлежащие одному классу, образуют разрешенную комбинацию при установке встык. Поиск таких групп сводится крешению задачи на графе.16Неориентированный граф определен как, в котором —множество вершин, — множество ребер.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
