Диссертация (Исследование и разработка методов автоматического вывода геометрических ограничений с использованием декларативного программирования и формальных методов), страница 9

Использованиесовременных формальных методов и декларативного программированияпозволяет сократить временные и трудовые затраты на поиск решения,38удовлетворяющего заданным критериям качества. Использование подобноговычислительного комплекса позволяет сократить разрыв между этапамилогического и физического проектирования СБИС.39Глава 2. Математическое обеспечение вычислительного комплексаавтоматического вывода геометрических ограниченийВ диссертационной работе предлагается использовать формальные методыи декларативное программирование для решения задачи из области разработкимикро- и наноэлектроники. На первом этапе необходимо разработать модельпредставления геометрических данных.

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

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

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

. . или же буквамис индексами, например, x1 . Над заданными переменными выполняютсяследующие операции: логическое И (∧), ИЛИ (∨), отрицание (¬), импликация (→)и эквиваленция (↔). Скобки используются для изменения приоритетов операций.Пусть B := 0,1 — множество бинарных значений. Bn описывает бинарныйn–мерный куб, где каждый элемент e = (e0 , . . . ,en ) называется конъюнктивнымодночленом или минтермом. Примером множества B является булева алгебра, вкоторой B дополнено операциями дизъюнкции и конъюнкции.

Булевой функциейf от n переменных x1 , . . . , xn называется следующее отображение:f : Bn → {0, 1, −},где символ − соответствует значению “не важно”. Терм e соответствуетзначениям переменных функции f , например, x1 = e1 , x2 = e2 , . . .. Включенным(англ. ON-set) множеством булевой функции f называется такое множествотермов, для которых f имеет значение Истина. Аналогично, выключенным(англ.

OFF-set) и “неважным” (англ. don’t care, DC) множествами являютсятакие множества термов, для которых f возвращает значения Ложьи “неважно”,соответственно.Определение выше описывает функции с одним выходным значением.Функции, имеющие несколько выходных значений, описываются следующимотображением:f : Bn → {0, 1, −}m.41Стоит отметить, что каждый выход f1 , . . . ,fm имеет свои собственные ON,OFF и DC множества. Далее будут рассмотрены, без потери общности, толькофункции с одним выходом.Каждая переменная xi имеет два ассоциированных с ней литерала:позитивный xi и негативный ¬xi . Литерал может принимать значениеИстина или Ложь.

Каждый литерал соответствует термам, для которых булевафункция возвращает значение Истина (Ложь) для термов с ei = 1 и значениеЛожь (Истина) для термов с ei = 0. Конъюнкция литералов также называетсялогическим произведением. Такое произведение возвращает значениеИстина(включает минтерм e) в случае, если все литералы заданного минтерматакже имеют значение Истина, иначе произведение равно Ложь. Стоит отметить,что каждый минтерм соответствует только такому произведению, которое еговключает.

Таким образом, минтерм e = (e1 , . . . , en ) соответствует произведениюxe1n , . . . , xenn , в котором xei i обозначает литерал xi или его комплементарныйлитерал ¬xi для ei = 1(0). Например, минтерму e = (1,0,1) соответствуетпроизведение x1 ¬x2 x3 .

Так как произведение соответствует множеству смежныхминтермов в бинарном n-мерном кубе, то его нередко называют кубом.Говорят, что куб α входит в куб β (α ⊆ β), если каждый минтерм в α такжевходит в β. Пересечение кубов α и β (α∪β) единственным образом определяет куб,в который входят минтермы из обоих кубов. Суперкубом кубов α и β называютединсвтенным образом определяют куб минимального размера, включающий всебя оба куба. Например, для α = x1 ¬x2 и β = ¬x1 ¬x2 x3 суперкубом является¬x2 .

Для построения суперкуба необходимо рассмотреть все литералы, в суперкубвходят те из них, которые входят в оба заданных куба.Конъюнктивной нормальной формой (КНФ) называется дизъюнкцийконъюнктов. КНФ возвращает значение Истина в случае, если хотя быодин конъюнкт содержит заданный минтерм.

Импликантом булевой функцииназывается такой куб, который не содержит минтермов из OFF множества.Простой импликант не содержит никаких других импликантов функции.Необходимый просто импликант включает в себя не менее одного минтермаиз множества ON, который не входит ни в какой другой простой импликант.Покрытием булевой функции называется такое множество импликантов в формеКНФ, которая возвращает значение Истина для всех минтермов множества ON42и ни для одного из OFF множества. Простым называется покрытие, в котороевходят только простые импликанты.Каждой логической переменной p сопоставляется два литерала (англ.

literal)(pi , ¬pi ), соответствующие двум возможным значениям логической переменной p.Утверждением (англ. clause) называется такая дизъюнкция литералов{p0 , p1 , . . . , pn }, которая содержит только уникальные литералы и не содержиткомплиментарные пары литералов (pi , ¬pi ). Утверждения записываются в видеформулы p0 ∨ p1 ∨ · · · ∨ pn . Множество дизъюнкций F обозначает конъюнкциюутверждений или, иначе говоря, КНФ.Значение утверждения p0 ∨ p1 ∨ .

. . ∨ pn соответствует Истина (1),если значение хотя бы один из литералов равно Истина, иначе оно равноЛожь (0). Пустое утвеждение n = 0 также соответствует значению Ложь.Значение всей формулы F равно Истина, если каждое утверждение имеетзначение Истина, иначе ее значение равно Ложь. Множество утвержденийF называется выполнимым, если существует хотя бы один набор значенийвходных параметров, при котором F возращает значение Истина, иначе Fназывается невыполнимой. Множество входных параметров, выполняющих F ,также называется моделью. КНФ, содержащая только пустые утверждения,считается невыполнимой. Любому выражению логики высказываний F′′соответствует выражение F в виде КНФ, такое, что если F выполнима,то может F также может быть выполнена [59].Задача “распознавания” может быть сформулирована следующимобразом: может ли быть выполнена заданная формула F ? Эта задача первая, длякоторой была доказана принадлежность к классу задач N P –полных [60].Все известные алгоритмы для решения этой задачи могут потребоватьэкспоненциально много времени в зависимости от размера формулы.

Вопрос,существуют ли полиномиальные алгоритмы решения N P -полных задач, являетсяоткрытым.Принаделженость SAT задачи к классу N P -полных позволяет заключить,что множество других проблем могут быть представлены в виде SAT задачи.Примерами такой трансляции могут служить задачи трассировки [51; 54],размещения [50], расщепления транзисторов [61].Все алгоритмы решения SAT могут быть разделены на полные инеполные. Алгоритмы, принадлежащие к первой группе, помимо нахождения43модели и доказательства выполнимости входной КНФ формулы, могут такжепредоставить доказательство невыполнимости заданной формулы при любыхзначениях входных параметров.

Алгоритмы второй группы, неполные, какправило используют методы локального поиска для поиска моделей.2.1.1DPLL алгоритмЦентральное место в методах решения SAT задач занимають алгоритмыDPLL и его расширение CDCL. Первоначальная версия DPLL алгоритма былапредставлена в работе [62] и основывалась на правиле резолюций. В статье [63]предложенный алгоритм был модифицирован с целью сокращения потребленияпамяти.DPLL алгоритм опирается на следующие процедуры:– Распространение переменной. Если есть утверждение единичнойдлины c = pi , то необходимо добавить литерал pi в модель. Все остальныеутверждения, содержащие pi , могут быть удалены из КНФ, литерал ¬piдолжен быть удален из всех утверждений.– Присвоение чистой переменной.