Аннотации курсов

ДНМ05
Сложность комбинаторных алгоритмов

Рассматриваются общие модели и утверждения о сложности комбинаторных задач, методы построения быстрых алгоритмов (метод динамического программирования, «разделяй и властвуй», «метод расширения модели»). Приводятся примеры применения этих методов с оценками их сложности, даются основные «сложностные» классы задач и примеры универсальных в этих классах задач.

СДМ01
Элементы теории синтеза и сложности дискретных управляющих систем

Краткая аннотация курса. Рассматриваются методы синтеза и получения нижних оценок сложности для ряда конкретных функций, встречающихся в приложениях. Решаются дополнительные задачи синтеза, связанные с изучением поведения функций Шеннона на уровне асимптотических оценок высокой степени точности, а также с синтезом схем для функций из специальных классов. Изучается ряд вопросов геометрической реализации схем.

СДМ02
Математические модели и методы синтеза СБИС

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

СДМ03
Математические модели задач физического проектирования микросхем (Electric Design Automation)

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

СДМ04
Вычислительная линейная алгебра задач большой размерности

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

В курсе рассматриваются: схемы хранения и основные операции над разреженными матрицами; решение линейных систем прямыми методами (симметричные и несимметричные системы); решение линейных систем итерационными методами (симметричные и несимметричные системы); выбор подходящего итерационного метода. Излагаются общие вопросы теории и практики итерационных методов (скорость сходимости, достижимая точность, критерии останова и пр.), вопросы, связанные с предобусловливанием линейных систем. Рассматриваются задачи на собственные значения (симметричные и несимметричные).

СДМ05
Решение булевых уравнений и проблемы выполнимости

Учебный курс состоит из двух разделов.

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

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

СДМ06
Теория надежности и контроля схем. Методы построения тестов

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

СДМ07
Дополнительные вопросы теории графов и комбинаторики.

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

СДМ08
Языки описания схем. Проблемы верификации

Первая часть курса посвящена современным языкам описания микроэлектронных схем, используемым в системах автоматизированного проектирования СБИС. В этой части курса слушатели накомятся с принципами устройства языков описания схем, с основными конструкциями, функциональными и декларативными возможностями этих языков, с практическим применением указанных языков в рамках одной из САПР СБИС.

Во второй части курса рассматривается математический подход к решению задачи проверки правильности функционирования распределенных программ (систем взаимодействующих процессов, сетевых протоколов, микроэлектронных схем и др.) - верификация моделей программ (model checking). Слушатели знакомятся с базовыми принципами этого подхода, с языками темпоральных логик, используемых для формальной спецификации поведения систем взаимодействующих процессов, с алгоритмами проверки выполнимости формул темпоральных логик на конечных моделях.