Разложение определителя по ряду. Минор и алгебраическое дополнение к элементу определителя. Связь алгебраических дополнений с минорами — Студопедия
Поделись
Пусть Δ = = .
Определение 1. Если в определителе Δ сгруппировать все слагаемые, содержащие элемент aij и, сгруппировав, вынести элемент aij за скобки, то выражение, полученное в скобках, обозначается Aij и называется алгебраическим дополнением к элементу aij в определителе Δ, i = , j = .
Так как все элементы i-той строки определителя Δ входят в одно и только одно из слагаемых, то Δ=ai1Ai1+ ai2Ai2+ … + ainAin (1). Равенство (1) называется разложением определителя Δ по i-той строке.
Аналогично: Δ=a1jA1j+ a2jA2j+ … + anjAnj (2) — разложение определителя Δ по j-тому столбцу, j =.
Строки и столбцы определителя Δ называются его рядами. Таким образом, (1) и (2) – разложения Δ по ряду.
Определение 2. Если в определителе Δ вычеркнуть i-тую строку и j-тый столбец, то на их пересечении получится элемент aij, а остальные элементы образуют определитель (n-1)-го порядка, который обозначается Mij и называется минором к элементу aij в определителе Δ, i = , j = .
Пример 1. Пусть Δ = . Тогда M23 =и т.д.
Теорема 1. ПустьΔ — определитель n-гопорядка над полем P, Aij и Mij – алгебраическое дополнение и минор к элементу aijвΔсоответственно.Тогда
Aij=(-1)i+ jMij, i = , j = .
Доказательство. Пусть Δ1 — сумма всех тех слагаемых из Δ, которые содержат элемент aij, т. е. Δ1== (3). Вторые индексы в (3) образуют перестановку I1, полученную из перестановки I удалением символа j с i-того места. Тогда, по теореме о четности перестановки, получим = =aij(-1)i+jMij, т.е. Δ1 = aij(-1)i+jMij (4). С другой стороны Δ1 =aijAij(5). Из (4) и (5) следует, что aij(-1)i+jMij = aijAij. Тогда Aij = (-1)i+jMij. Теорема доказана.
6. Свойства определителей.
Свойство 1.
Доказательство. Пусть — матрица n-го порядка над полем Р. Транспонируя А, получим . Всевозможные произведения вида будут одинаковыми как для матрицы А, так и для матрицы tА. При этом знак произведения сохраняется. Таким образом, ∣А∣=∣tА∣.
Из свойства 1 следует, что все утверждения, справедливые для какой-либо строки определителя, верны и для его столбца
Свойство 2. Если все элементы некоторой строки определителя равны нулю, то определитель равен нулю.
Доказательство. В каждое произведение определителя обязательно входит один элемент строки, состоящей из нулей. Поэтому все слагаемые определителя раны нулю, а, значит, и определитель равен нулю.
Свойство 3. От перестановки двух строк местами определитель меняет знак.
Доказательство. Пусть Δ = .
В определителе Δ переставим i-ю и j-ю (i<j) строки местами. Получим:
Δ ‘= . Пусть — одно из произведений определителя Δ. Тогда соответствующим для определителя Δ’ будет произведение . Эти произведения различаются только индексами сомножителей. Перестановка (k1 k2 … kj … ki … kn) получена из перестановки (k1 k2 … ki … kj … kn). Такое преобразование меняет четность перестановки, а, следовательно, знак рассматриваемого произведения. Таким образом, при перестановке двух строк местами все произведения, составляющие определитель Δ, поменяют знак. Следовательно, поменяет знак и Δ.
Свойство 4. Определитель, содержащий две одинаковые строки, равен нулю.
Доказательство. Пусть определитель Δ содержит две одинаковые строки: i-ю и j-ю. Поменяем их местами. По свойству 3, определитель Δ поменяет знак: Δ’=—Δ. Но, так как строки одинаковые, то Δ’=Δ. Значит, Δ=—Δ и Δ=0. Свойство доказано.
Свойство 5. Общий множитель всех элементов некоторой строки определителя можно вынести за знак определителя.
Доказательство. Δ = = . Пусть элементы i-ой строки имеют общий множитель α. Так как в каждое слагаемое вида входит элемент этой строки, то все такие произведения имеют общий множитель α, который можно вынести за знак всей суммы в Δ.
Свойство 5′. Если все элементы некоторой строки определителя Δ умножить на одно и тоже число, то определитель умножится на это число.
Свойство 6. Определитель, содержащий две пропорциональные строки, равен нулю.
Доказательство. Пусть Δ = , причем ai1=aj1, ai2=aj2, …, ain=ajn. Вынесем элемент α из j-ой строки за знак определителя Δ. Получим:
Δ = . Тогда, по свойству 4, Δ =α⋅0=0.
Свойство 7. Если все элементы i-ой строки определителя представлены в виде суммы двух слагаемых, то определитель равен сумме двух определителей, у которых все строки, кроме i-ой, те же, что и у данного определителя, i-я строка одного определителя состоит из первых слагаемых i-ой строки данного определителя, а i-я строка второго – из вторых слагаемых i-ой строки данного определителя.
Свойство 8. Определитель не изменится, если к элементам одной строки прибавить соответствующие элементы другой строки, умноженные на одно и то же число.
Свойство 9. Сумма произведений элементов какой-либо строки определителя n-го порядка на алгебраические дополнения соответствующих элементов другой строки равна нулю, то есть ai1Aj1+ai2Aj2+…+ainAjn=0 где i≠j.
Миноры. Алгебраические дополнения. Разложение определителя по элементам строки (столбца)
Опр. Определитель матрицы, получаемой при вычеркивании матрицы А нескольких строк и столбцов, называется минором матрицы А.
Очевидно, что надо вычеркивать столько строк и столбцов, чтобы оставшаяся матрица была квадратной, иначе нельзя найти ее определитель. Если матрица А была квадратной, то вычеркиваются одинаковое число строк и столбцов. Если вычеркиваем i-ю строку и j-й столбец, то минор обозначается Мij и называется минором элемента а ij, стоящего на пересечении i-й строки и j-го столбца.
Опр. Число Аij=(-1)i+jMij называется алгебраическим дополнением элемента аij .
Теорема. Если ,то и это представление называется разложением определителя по элементамi-й строки.
Доказательство. 1. Рассмотрим сначала случай
,
т.е. при. Тогда
2. Рассмотрим случай , т.е. вi-й строке только элемент j-го столбца может отличаться от нуля. Тогда i-ю строку переставляя с соседними переводим на первую строку. При этом знак определителя меняется i-1 раз. Далее, j-й столбец переводим на первый столбец, переставляя с соседними столбцами. При этом знак определителя меняется j-1 раз. Итак, учитывая предыдущий случай, получим .
3. Общий случай. Представим определитель |A| как сумму определителей |Ak| таких, что у всех определителей строки, за исключением i-й строки, совпадают со строками определителя |A|.
,
что требовалось доказать.
Замечание. Определитель можно разлагать и по элементам столбца.
Следствие. Сумма произведений элементов строки (столбца) на алгебраические дополнения соответствующих элементов другой строки (столбца) равна нулю.
Доказательство. Действительно, сумма представляет разложение поk- й строке определителя, у которого k-я строка совпала с i-й строкой. А определитель с двумя одинаковыми строками равен нулю.
Пример. Найти определитель .
Разлагаем по элементам 1-го столбца. Получим
|A|=2(-1)1+12(12+8+30+10-48+6)-3()3+0+45-0- 12+9=36-135=-99.
Опр. Пусть А – матрица n-го порядка. Матрица А -1 называется обратной к А, если А-1А=АА-1=Е. если существует А-1, то А называется обратимой.
Замечание. Если А-1 существует, то она единственная.
Действительно, пусть А’ другая, обратная к А. тогда умножая А-1А=Е на А’ справа получим
(А-1А)А’=ЕА’А-1(АА’)=А’А-1Е=А’ A-1=A’, что требовалось доказать.
Теорема. А-1 существует тогда и только тогда, когда det A0 (если det A0, то матрица А называется невырожденной).
Док—во. Необходимость. Дано, что А-1 существует. Тогда АА-1=Е|A||A-1|=|E|=1. Значит, |A| 0, иначе 0=1, что невозможно.
Достаточность. Дано, что |A| 0. Заменим в матрице А все элементы их алгебраическими дополнениями. Полученная матрица называется присоединенной матрицей. Транспонируем присоединенную матрицу и разделим каждый ее элемент на =|A| 0. Проверим, что получили обратную матрицу. Элемент сik произведения
имеет вид
.
При i=k в числителе имеем разложение |A| по k-й строке, поэтому сkk=/=1. Приik в числителе имеем сумму произведений элементов i-й строки на алгебраические дополнения элементов другой k-й строки, что дает нуль. Итак, сik=0 при ik. Значит, АА-1=Е. Аналогично проверяется, что А-1А=Е.
Пример. Найти А-1, если она существует, А=.
Имеем |A|= -3+6+0-8-2-0= -70. Значит, А-1 существует.
= -5, = -17, А13= -1,
А21= -(-2)=2, А22=11, А23= -1,
А31=2, А32= -(-4)=4, А33= -1.
Тогда присоединенная матрица имеет вид
.
Транспонируем и делим все элементы на |A|= -7. Получим обратную матрицу
.
Выбор порядка переменных для цилиндрической алгебраической декомпозиции с искусственными нейронными сетями
Математическое программное обеспечение — ICMS 2020. 6 июня 2020 г.; 12097: 281–291.
Опубликовано в сети 6 июня 2020 г. doi: 10.1007/978-3-030-52200-1_28
PMCID: PMC7340889
Приглашенный редактор (ы): Анна Мария Бигатти, 8 9 Джеймс H09009, Жак Каретт, Давенпорт, 10 Майкл Джосвиг, 11 и Тимо де Вольф 12
8 Кафедра математики, Università degli Studi di Genova, Genova, Genova Italy
9 Computing and Software, McMaster University, Hamilton, ON Канада
10 Факультет компьютерных наук, Университет Бата Великобритания
11 Институт математики, MA 6-2, Технический университет Берлина, Берлин, Германия
12 Технический университет Брауншвейга, Брауншвейг, Германия
Анна Мария Бигатти, Эл.
Информация об авторе.
, 13, 14 , 13 и 13, 14
Информация об авторе Информация об авторских правах и лицензии Цилиндрическая алгебраическая декомпозиция (CAD) является основным инструментом вычислительной реальной алгебраической геометрии. Предыдущие исследования показали, что подходы, основанные на машинном обучении (ML), могут превзойти традиционные эвристические подходы при выборе наилучшего порядка переменных, когда количество переменных . Одной из основных проблем при обработке общего случая является экспоненциальный рост количества различных порядков, когда n увеличивается. В этой статье мы предлагаем итеративный метод для создания возможных порядков переменных и подход ML для выбора из них наилучшего порядка с помощью обучения классификаторов нейронных сетей. Эксперименты показывают, что этот подход превосходит эвристические для .
Ключевые слова: Цилиндрическая алгебраическая декомпозиция, Порядок переменных, Машинное обучение, Нейронная сеть
Цилиндрическая алгебраическая декомпозиция (CAD) была введена Коллинзом для решения задач исключения реальных кванторов [14]. Первоначальная структура для вычислений САПР, представленная Коллинзом, основана на схеме проекции и подъема, которая в настоящее время постепенно улучшается многими другими [1, 3, 5, 19]. –23]. В 2009 году Морено Маза, Ся, Ян и первый автор [13] предложили новый способ вычисления САПР, который сначала вычисляет цилиндрическую декомпозицию сложного пространства, а затем преобразует ее в САПР реального пространства на основе техники треугольной декомпозиции. и регулярные цепочки [13]. Его эффективность была существенно улучшена в [7] на основе пошагового алгоритма, который также может использовать ограничения по уравнениям. Полный и эффективный алгоритм исключения вещественных кванторов на его основе был предложен в [12]. Кроме того, он может использовать дизъюнктивные эквациональные ограничения путем вычисления таблицы истинности, инвариантной САПР [2].
Сегодня, несмотря на свою удвоенную экспоненциальную сложность [6, 14], САПР эффективно реализована во многих программах, таких как QEPCAD, Mathematica, REDLOG и Maple, и нашла широкое применение в доказательстве геометрических теорем, анализе устойчивости динамических систем, управлении проектирование систем, проверка гибридных систем, проверка программ, нелинейная оптимизация, автоматическое распараллеливание и т. д. В последнее время он также находит применение при изучении квантовой нелокальности [8].
Было показано, что выбор порядка переменных оказывает большое влияние на производительность САПР как теоретически [6], так и на практике [15]. Было предложено несколько эвристических методов выбора порядка переменных. В частности, две эвристические стратегии [4, 9] реализованы в команде SuggestVariableOrder (SVO) библиотеки RegularChains в Maple. С другой стороны, естественным вариантом также становится прогнозирование наилучшего порядка переменных с помощью подходов искусственного интеллекта, среди которых машинное обучение является естественным выбором [16–18, 24, 25].
Существующая работа по выбору порядка переменных с помощью машинного обучения сосредоточена на трехмерном случае. Для более чем трех переменных становится сложнее получить достаточное количество размеченных данных из-за двойного экспоненциального поведения САПР по количеству переменных и . Другая трудность заключается в экспоненциальном росте числа различных порядков при увеличении на . В этой статье мы сначала предлагаем итеративный подход для создания лучшего порядка переменных, начиная с того, который задан SVO. Затем уменьшаем потенциал на ! количество классов для прогнозирования задачи упорядочения переменных до n путем обучения классификатора нейронной сети данными, сгенерированными с помощью итеративного подхода. Эксперименты показывают, что как итеративный подход, так и подход машинного обучения превосходят SVO для .
Организация статьи следующая. В разд. 2 мы кратко рассмотрим концепцию САПР и проблему выбора порядка переменных. В разд. 3 и разд. 4 мы представляем соответственно подходы итеративного и машинного обучения. В разд. 5 мы экспериментально показываем эффективность наших подходов. Наконец, мы делаем вывод в разд. 6.
Рассмотрим набор полиномов и порядок переменных . F -инвариантная цилиндрическая алгебраическая декомпозиция (CAD) разбивает на непересекающиеся и цилиндрически расположенные полуалгебраические подмножества (называемые ячейками) так, что проекция любых двух ячеек на (с координатными переменными) либо не пересекается, либо тождественно равна. Порядок переменных также определяет порядок исключения переменных и порядок построения САПР из проекционных факторов или сложной цилиндрической декомпозиции.
Представленные в [2, 10, 13] алгоритмы расчета САПР на основе регулярных цепочек были реализованы в команде CylindricalAlgebraicDecompose в библиотеке RegularChains Maple [11]. Его последняя версия доступна на http://www.regularchains.org, и мы используем версию с http://www.arcnl.org/cchen/software/cadorder. В библиотеке RegularChains команда SuggestVariableOrder (сокращенно SVO) реализует два разных эвристических метода выбора порядка переменных, а именно метод Брауна [4] (с параметром «разложение = cad», сокращенно SVO(B)) и метод Чен и др. [9] (параметр по умолчанию, сокращенно SVO(C)).
Порядок переменных играет важную роль в эффективности вычислений САПР, как показано в следующем примере.
Пример 1
Пусть В таблице указано время вычислений и количество ячеек для нескольких переменных порядков. Как мы видим, в этом примере современные эвристические методы избегают выбора худшего порядка переменных, но также пропускают лучший порядок переменных.
Таблица 1.
Влияние различных переменных порядков
Order | Method | Timing (seconds) | cells |
---|---|---|---|
– | 5 | 3373 | |
– | 93 | 43235 | |
SVO (B) | 16 | 11953 | |
SVO (C) | 14 | 9253 | 9253 |
. 0003
В этом разделе мы представляем итеративный метод выбора порядка переменных, называемый IVO, для цилиндрической алгебраической декомпозиции. Он начинается с первоначального заказа, предоставленного SVO. Затем он вызывает подпрограмму, называемую RVO, для генерации n порядков в циклическом режиме и выбирает лучший, вычисляя с ним кратчайшее время вычисления САПР. Затем он фиксирует самую большую переменную и снова вызывает RVO для остальных, чтобы выбрать вторую по величине переменную, и так далее. Точное описание и приведены ниже. Обозначим через || объединение двух последовательностей.
Алгоритм РВО.
Ввод: набор многочленов F ; последовательность переменных O , определяющая порядок по убыванию; время t для работы, целое число k .
Вывод: новый порядок и время работы, такое что .
Шаги:
Пусть и .
Пусть , .
Для каждого позвоните и запишите время работы.
Сравните это время работы с t и верните самое короткое время и соответствующий порядок.
Алгоритм ИВО.
Ввод: набор многочленов F ; последовательность переменных X .
Вывод: перестановка X , которая определяет убывающий порядок переменных.
Шаги:
Если , вернуть х .
Пусть и .
Пусть t будет более коротким временем выполнения между и и пусть O будет соответствующим заказом с более коротким временем (если они равны, мы используем ).
Для к от 0 до
.
Возврат O .
Легко видеть, что в большинстве случаев это вызывает CAD. В оставшейся части этой статьи, если не возникнет путаницы, мы будем обозначать через SVO(*) оракул, который всегда возвращает лучший порядок между и и через SVO любой из трех.
Чтобы обучить полезную модель машинного обучения для прогнозирования наилучшего порядка переменных для САПР, важно иметь набор данных с достаточным количеством помеченных примеров, а размер набора данных не может быть слишком маленьким. С другой стороны, поскольку вычисления в САПР обходятся дорого, когда количество переменных превышает 3, больший набор данных требует больше вычислительных ресурсов. Чтобы сделать изученную модель полезной, лучше, чтобы обучающий набор данных содержал разнообразные примеры. С другой стороны, если данные слишком разнообразны, учиться будет сложно. В следующей таблице обобщена информация о наборе данных, который мы генерируем, используя случайные полиномы в качестве входных данных для IVO. Весь набор данных разделен на три набора данных, используемых соответственно для обучения, проверки и тестирования с коэффициентом 9./1/1. Набор данных проверки используется для настройки модели машинного обучения, в то время как набор данных тестирования обрабатывается как невидимые данные, используемые только один раз для сообщения экспериментальных результатов в документе и демонстрации способности модели ML к обобщению.
Данные в таблице были сгенерированы на кластере (4 вычислительных узла, каждый из которых имеет два процессора Intel E5-2620 (по 6 ядер каждый) и 64 ГБ памяти). На каждом узле параллельно запускалось 6 сессий Maple. Ограничение по времени установлено как 15 мин. Общее время создания набора данных составляет около 1 месяца. В таблице мы записываем только количество допустимых примеров. Пример действителен, если CAD завершает вычисление в срок хотя бы для одного заказа, вычисленного IVO. Обратите внимание, что возможно, что SVO возвращает заказ, для которого истекает время ожидания CAD.
Table 2.
Dataset
n | Degree | terms | polynomials | Equations | #valid examples |
---|---|---|---|---|---|
4 | 2..3 | 2..5 | 2 | No | 10957 |
5 | 2..3 | 3..6 | 2 | No | 6875 |
6 | 2. .3 | 4. .6 | 2 | Нет | 3751 |
Открыть в отдельном окне
Далее мы вспоминаем особенности представления многочленов, введенные в нашей предыдущей работе [24]. Эти функции генерируются на основе структуры графа, определенной для полиномиальных систем. Для данной переменной эквивалентное описание функций сведено в следующую таблицу . Пусть E ( i ) будут функциями, связанными с . Затем вектор признаков.
Table 3.
Features
Feature | Description |
---|---|
, где lc обозначает старший коэффициент | |
Откроем в отдельном окне переменную, которая может тренировать заказы
3 90. Вместо того, чтобы рассматривать порядок переменных как класс, что может привести к огромному количеству классов для фиксированных n , мы хотели бы обучить мультиклассовый классификатор, который предсказывает только самую большую переменную в порядке. Чтобы достичь этого, для каждого примера в наборе данных мы будем вызывать SVO, чтобы вернуть первоначальный порядок, а затем вызывать один раз, чтобы получить, как мы надеемся, лучший порядок. Затем первая переменная в упорядочении устанавливается как метка примера. Для каждого мы обучаем модель классификации искусственной нейронной сети, реализованную в TensorFlow. Структура и параметры нейронной сети проиллюстрированы на рис. Каждый из них представляет собой полносвязную нейронную сеть с одним входным слоем, тремя скрытыми слоями и одним выходным слоем softmax. Используемая функция активации — ReLu. Гиперпараметры сети настраиваются вручную для максимальной точности проверки.
Открыть в отдельном окне
Нейросетевой классификатор
Предположим, мы получили хорошо обученные модели , . Затем мы используем следующую процедуру PVO для предсказания порядка переменных.
Алгоритм PVO
Вход: набор полиномов F ; последовательность из n переменных X .
Вывод: перестановка X , которая определяет убывающий порядок переменных.
Шаги:
Вычислить последовательность векторов признаков для F .
Пусть .
Пусть .
Возврат .
Общий процесс обучения и прогнозирования показан на рис.
Открыть в отдельном окне
Блок-граф поиска переменной порядка на основе искусственной нейронной сети.
В этом разделе мы сообщаем об экспериментальных результатах итеративного метода и подхода машинного обучения для выбора порядка переменных.
Обратите внимание, что при вызове для прогнозирования порядка переменных у нас есть три варианта. Можно использовать или получить первоначальный заказ без вызова САПР. Или можно использовать SVO(*) для получения лучшего результата между и , но для этого требуется дважды вызывать CAD. Тем не менее, для мы используем и для обозначения итерационного метода, первую итерацию итерационного метода и метод на основе ML для выбора порядка переменных, который использует в качестве начального порядка. В результате набор данных для тестирования представляет собой, соответственно, набор примеров, для которых обеспечивается начальное упорядочение в исходном наборе данных для тестирования. В таблице указан размер наборов данных. Обратите внимание, что набор данных для не содержит примеров тайм-аута. Это связано с тем, что всякий раз, когда CAD истечет с порядком, заданным , будет использовать порядок, заданный . Хотя тестовые наборы данных и процедуры вывода для и различаются, для данного n , оба и используют один и тот же классификатор, обученный с набором данных в таблице, где примеры помечены RVO (*) с начальным порядком переменных, заданным SVO (*). В таблице приведены среднее время вычислений (в секундах) и время ожидания IVO(*) и RVO(*) для всех наборов данных. Обратите внимание, что наборы данных содержат только примеры, в которых IVO(*) работает успешно.
Таблица 4.
Размер тестовых наборов данных
n | B | C | n | B | C | n | B | C | |||
---|---|---|---|---|---|---|---|---|---|---|---|
4 | 593 | 404 | 997 | 5 | 359 | 266 | 625 | 6 | 214 | 127 | 341 |
Открыть в отдельном окне
На рисунке показана точность шести методов выбора упорядочения. Здесь основная истина для SVO(a) и PVO(a) определяется как , для . Точность определяется как процент лучших порядков, выбранных каждым методом, по отношению к общему количеству тестовых примеров, приведенных в таблице. Заметим, что точность PVO(a) выше, чем SVO(a) при , для всех . При точность PVO(a) несколько ниже, чем SVO(a) при и выше, чем SVO(a) при .
Открыть в отдельном окне
Точность различных методов выбора порядка
На рисунке показано среднее время работы САПР с переменным порядком, предсказанным различными методами. Если есть тайм-аут, время засчитывается как удвоенный лимит времени, то есть полчаса. Для и среднее время вычисления PVO(a) значительно меньше, чем SVO(a). Среднее время вычисления PVO(C) меньше, чем SVO(C) для , но больше, чем SVO(C) для .
Открыть в отдельном окне
Среднее время работы САПР с различным порядком переменных
На рисунке показан процент тайм-аутов для CAD с порядком переменных, предсказанным разными методами. Явление здесь похоже на время вычисления, как показано на рис. .
Открыть в отдельном окне
Примеры тайм-аутов в процентах для САПР с различным порядком переменных
В этой статье мы предлагаем основанный на машинном обучении подход для прогнозирования наилучшего порядка переменных для САПР, предназначенного для . Эксперименты показывают, что он превосходит традиционные эвристические подходы для случайно сгенерированных наборов данных. Команда CylindricalAlgebebraicDecompose может вычислять в САПР еще более крупные n , скажем, за разумное время, если в системе есть несколько эквациональных ограничений [7]. Будет интересно расширить модель для , протестировать ее на задачах CAD-QE из реальных приложений и, наконец, сделать метод выбора упорядочения переменных на основе ML полезной опцией для SuggestVariableOrder. Данные и код, используемые в этой статье, доступны по адресу http://doi.org/10.5281/zenodo.3818086.
Авторы благодарят анонимных рецензентов за полезные комментарии. Это исследование было поддержано NSFC (11771421, 11671377, 61572024), программой CAS «Свет Западного Китая», Ключевой исследовательской программой передовых наук CAS (QYZDB-SSW-SYS026) и cstc2018jcyj-yszxX0002 из Чунцина.
Анна Мария Бигатти, электронная почта: ti.eginu.amid@ittagib.
Жак Каретт, электронная почта: ac.retsamcm@etterac.
Джеймс Х. Давенпорт, электронная почта: [email protected].
Майкл Йосвиг, электронная почта: ed.nilreb-ut.htam@giwsoj.
Тимо де Вольф, электронная почта: [email protected].
1. Арнон Д.С., Коллинз Г.Е., МакКаллум С. Цилиндрическая алгебраическая декомпозиция I: основной алгоритм. СИАМ Дж. Вычисл. 1984; 13(4):865–877. дои: 10.1137/0213054. [Перекрестная ссылка] [Академия Google]
2. Брэдфорд Р., Чен С., Давенпорт Дж. Х., Ингланд М., Морено Маза М., Уилсон Д. Инвариантная таблица истинности цилиндрическая алгебраическая декомпозиция с помощью регулярных цепей. В: Гердт В.П., Копф В., Зайлер В.М., Ворожцов Е.В., ред. Компьютерная алгебра в научных вычислениях; Чам: Спрингер; 2014. С. 44–58. [Google Scholar]
3. Брэдфорд Р.Дж., Дэвенпорт Дж.Х., Ингленд М., МакКаллум С., Уилсон Д.Дж. Инвариантная таблица истинности цилиндрическая алгебраическая декомпозиция. Дж. Симб. вычисл. 2016; 76:1–35. doi: 10.1016/j.jsc.2015.11.002. [Перекрестная ссылка] [Академия Google]
4. Браун, К.: Учебник: Цилиндрическая алгебраическая декомпозиция, в ISSAC (2004). http://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf
5. Браун CW. Улучшенная проекция для цилиндрической алгебраической декомпозиции. Дж. Симб. вычисл. 2001;32(5):447–465. doi: 10.1006/jsco.2001.0463. [CrossRef] [Google Scholar]
6. Браун, К.В., Давенпорт, Дж.Х.: Сложность устранения кванторов и цилиндрической алгебраической декомпозиции. В: Труды ISSAC, стр. 54–60 (2007)
7. Чен С., Морено Маза М. Инкрементальный алгоритм для вычисления цилиндрических алгебраических разложений. В: Feng R, Lee W, Sato Y, редакторы. компьютерная математика; Гейдельберг: Спрингер; 2014. С. 199–221. [Google Scholar]
8. Chen C, Ren C, Ye XJ, Chen JL. Критерии отображения между нелокальностью и управляемостью в системах кубит-кубит и между управляемостью и запутанностью в системах кубит-кудит. физ. Ред. А. 2018; 98(5):052114. doi: 10.1103/PhysRevA.98.052114. [Перекрестная ссылка] [Академия Google]
9. Чен С. и др.: Решение полуалгебраических систем с помощью библиотеки RegularChains в Maple. В: Труды MACIS, стр. 38–51 (2011). в полной версии
10. Чен С., Морено Маза М. Алгоритмы вычисления треугольной декомпозиции полиномиальных систем. Дж. Симб. вычисл. 2012;47(6):610–642. doi: 10.1016/j.jsc.2011.12.023. [CrossRef] [Google Scholar]
11. Чен С., Морено Маза М. Цилиндрическая алгебраическая декомпозиция в библиотеке RegularChains. В: Hong H, Yap C, редакторы. Математическое программное обеспечение – ICMS 2014; Гейдельберг: Спрингер; 2014. С. 425–433. [Академия Google]
12. Чен С., Морено Маза М. Исключение кванторов с помощью цилиндрической алгебраической декомпозиции на основе регулярных цепей. Дж. Симб. вычисл. 2016;75:74–93. doi: 10.1016/j.jsc.2015.11.008. [CrossRef] [Google Scholar]
13. Чен С., Морено Маза М., Ся Б., Ян Л.: Вычисление цилиндрической алгебраической декомпозиции с помощью треугольной декомпозиции. В: Proceedings of ISSAC, pp. 95–102 (2009)
14. Collins GE. Исключение кванторов для реальных замкнутых полей с помощью цилиндрической алгебраической декомпозиции. В: Brakhage H, редактор. Теория автоматов и формальные языки; Гейдельберг: Спрингер; 1975. стр. 134–183. [Google Scholar]
15. Дольцманн, А., Зайдл, А., Штурм, Т.: Эффективные заказы проекций для САПР. В: Труды ISSAC, стр. 111–118. ACM (2004)
16. England M, Florescu D. Сравнение моделей машинного обучения для выбора порядка переменных для цилиндрической алгебраической декомпозиции. В: Kaliszyk C, Brady E, Kohlhase A, Sacerdoti Coen C, редакторы. интеллектуальная компьютерная математика; Чам: Спрингер; 2019. С. 93–108. [Google Scholar]
17. Florescu D, England M. Улучшенная перекрестная проверка для классификаторов, которые делают алгоритмический выбор, чтобы минимизировать время выполнения без ущерба для правильности вывода. В: Сламаниг Д., Цигаридас Э., Зафейракопулос З., редакторы. Математические аспекты компьютерных и информационных наук; Чам: Спрингер; 2020. С. 341–356. [Академия Google]
18. Huang Z, England M, Wilson DJ, Bridge JP, Davenport JH, Paulson LC. Использование машинного обучения для улучшения цилиндрической алгебраической декомпозиции. Мат. вычисл. науч. 2019;13(4):461–488. doi: 10.1007/s11786-019-00394-8. [CrossRef] [Google Scholar]
19. Лазар Д. Улучшенная проекция для цилиндрической алгебраической декомпозиции. В: Bajaj CL, редактор. Алгебраическая геометрия и ее приложения. Нью-Йорк: Спрингер; 1994. С. 467–476. [Google Scholar]
20. МакКаллум С. Усовершенствованный оператор проектирования для цилиндрической алгебраической декомпозиции. В: Caviness B, Johnson J, редакторы. Исключение кванторов и цилиндрическая алгебраическая декомпозиция. Вена: Спрингер; 1998. стр. 242–268. [Google Scholar]
21. МакКаллум С., Парусински А., Паунеску Л. Доказательство достоверности метода Лазара для построения САПР. Дж. Симб. вычисл. 2019;92:52–69. doi: 10.1016/j.jsc.2017.12.002. [CrossRef] [Google Scholar]
22. Стржебоньски А. Решение систем строгих полиномиальных неравенств. Дж. Симб. вычисл. 2000;29(3):471–480. doi: 10.1006/jsco.1999.0327. [CrossRef] [Google Scholar]
23. Strzeboński A. Цилиндрическая алгебраическая декомпозиция с использованием проверенных чисел. Дж. Симб. вычисл. 2006;41(9): 1021–1038. doi: 10.1016/j.jsc.2006.06.004. [CrossRef] [Google Scholar]
24. Zhu, Z., Chen, C.: Выбор переменного порядка для цилиндрической алгебраической декомпозиции на основе машинного обучения. Дж. Сист. науч. Мат. (2018, принято). (на китайском языке)
25. Zhu, Z., Chen, C.: Выбор порядка переменных для цилиндрической алгебраической декомпозиции на основе иерархической нейронной сети. вычисл. науч. (2020, принято). (на китайском языке)
Цилиндрическая алгебраическая декомпозиция с уравнениями
- Англия, Мэтью ;
- Брэдфорд, Рассел ;
- Давенпорт, Джеймс Х.
Аннотация
Цилиндрическая алгебраическая декомпозиция (CAD) долгое время была одним из наиболее важных алгоритмов в символьных вычислениях как инструмент для выполнения исключения квантора в логике первого порядка над вещественными числами. В последнее время он находит известность в сообществе проверки выполнимости как инструмент для определения удовлетворительных решений задач в нелинейной действительной арифметике. Оригинальный алгоритм производит разложения по знакам полиномов, тогда как обычно требуется разложение по истинности формулы, содержащей эти полиномы. Один из подходов к достижению этой более грубой (но, надеюсь, более дешевой) декомпозиции состоит в том, чтобы сократить многочлены, идентифицированные в САПР, чтобы отразить логическую структуру, которая уменьшает размерность пространства решений: наличие уравнений уравнения (ECs). Эта статья может служить учебным пособием по использованию САПР с ЭК: мы описываем все необходимые предпосылки и текущее состояние дел. В частности, мы представляем недавнюю работу о том, как можно использовать теорию уменьшенной проекции МакКаллума для дополнительной экономии на этапе подъема: как полиномов, с помощью которых мы поднимаем, так и ячеек, которые поднимаются. Мы даем новый анализ сложности, чтобы продемонстрировать, что двойная экспонента в наихудшем случае, связанная со сложностью CAD, уменьшается в соответствии с количеством EC. Мы показываем, что редукция может применяться как к количеству получаемых многочленов, так и к их степени.