КАРТОЧКА ПРОЕКТА ФУНДАМЕНТАЛЬНЫХ И ПОИСКОВЫХ НАУЧНЫХ ИССЛЕДОВАНИЙ,
ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ
Информация подготовлена на основании данных из Информационно-аналитической системы РНФ, содержательная часть представлена в авторской редакции. Все права принадлежат авторам, использование или перепечатка материалов допустима только с предварительного согласия авторов.
ОБЩИЕ СВЕДЕНИЯ
Номер проекта 18-71-10042
НазваниеЗадачи выполнимости
Руководитель Куликов Александр Сергеевич, Доктор физико-математических наук
Организация финансирования, регион Федеральное государственное бюджетное учреждение науки Санкт-Петербургское отделение Математического института им. В. А. Стеклова Российской академии наук , г Санкт-Петербург
Конкурс №30 - Конкурс 2018 года по мероприятию «Проведение исследований научными группами под руководством молодых ученых» Президентской программы исследовательских проектов, реализуемых ведущими учеными, в том числе молодыми учеными
Область знания, основной код классификатора 01 - Математика, информатика и науки о системах; 01-101 - Математическая логика и основания математики
Ключевые слова Задача выполнимости, максимальная выполнимость, булева схема, формула, система доказательств
Код ГРНТИ27.03.45
ИНФОРМАЦИЯ ИЗ ЗАЯВКИ
Аннотация
Проект посвящен различным аспектам задачи выполнимости булевых формул и схем. В рамках проекта планируется построение алгоритмов для задачи выполнимости, с верхней оценкой времени работы лучше, чем у полного перебора, для некоторых классов формул или схем. Также планируется построение алгоритмов для вариантов задачи о максимальной выполнимости, в том числе параметрических алгоритмов для различных параметризаций. В рамках проекта планируется использовать алгоритмы для задачи выполнимости для построения оптимальных булевых схем для некоторых функций от небольшого количества аргументов, на основе которых можно построить достаточно эффективные булевы схемы для произвольного количества аргументов. Также планируется исследование систем доказательств, которые лежат в основе алгоритмов для задач выполнимости булевой формулы. В частности, планируется изучить исчисление ветвящихся программ.
ОТЧЁТНЫЕ МАТЕРИАЛЫ
Публикации
1. Лялина А. А. Верхняя оценка для задачи выполнимости булевых схем с единственным выполняющим набором Записки научных семинаров ПОМИ, т. 475, с. 122–137 (год публикации - 2018)
2.
Белова Т.С., Близнец И.А.
Upper and Lower Bounds for Different Parameterizations of (n,3)-MAXSAT
Lecture Notes in Computer Science, том 11346, с. 299–313 (год публикации - 2018)
10.1007/978-3-030-04651-4_20
3. Грязнов С. Notes on Resolution over Linear Equations Lecture Notes in Computer Science (год публикации - 2019)
4.
Куликов А.С., Михайлин И.А., Мохов А., Подольский В.В.
Complexity of Linear Operators
Proceedings of the 30th International Symposium on Algorithms and Computation (ISAAC 2019) (год публикации - 2019)
10.4230/LIPIcs.ISAAC.2019.17
5.
Белова Т.А., Близнец И.А.
Algorithms for (n,3)-MAXSAT and parametrization above the-all true assignment
Theoretical Computer Science (год публикации - 2020)
10.1016/j.tcs.2019.11.033
6. Лялина А.А On the Complexity of Unique Circuit SAT Journal of Mathematical Sciences, Vol. 247, No. 3, 457-466 (год публикации - 2020)
7. Басс С, Ицыксон Д.М., Кноп А.А., Рязанов А.А., Соколов Д.О. Lower Bounds on OBDD Proofs with Several Orders Electronic Colloquium on Computational Complexity (год публикации - 2020)
8.
Головнёв А.Г., Куликов А.С., Вильямс Р.
Circuit Depth Reductions
Leibniz International Proceedings in Informatics (Proceedings of 12th Innovations in Theoretical Computer Science Conference), 12th Innovations in Theoretical Computer Science Conference (ITCS 2021) стр 24:1--24:20 том 185 (год публикации - 2021)
10.4230/LIPIcs.ITCS.2021.24
9. Алферов В., Близнец И New Length Dependent Algorithm for Maximum Satisfiability Problem Thirty-Fifth AAAI Conference on Artificial Intelligence (год публикации - 2021)
10. Ицыксон Д.М., Рязанов А.А. Dmitry Itsykson, Artur Riazanov. Proof complexity of natural formulas via communication arguments Leibniz International Proceedings in Informatics (Proceedings of Computational Complexity Conference) (год публикации - 2021)
11. Софронова А.А., Соколов Д.О. Branching Programs with Bounded Repetitions and Flow Formulas Leibniz International Proceedings in Informatics (Proceedings of Computational Complexity Conference) (год публикации - 2021)
Публикации
1. Лялина А. А. Верхняя оценка для задачи выполнимости булевых схем с единственным выполняющим набором Записки научных семинаров ПОМИ, т. 475, с. 122–137 (год публикации - 2018)
2.
Белова Т.С., Близнец И.А.
Upper and Lower Bounds for Different Parameterizations of (n,3)-MAXSAT
Lecture Notes in Computer Science, том 11346, с. 299–313 (год публикации - 2018)
10.1007/978-3-030-04651-4_20
3. Грязнов С. Notes on Resolution over Linear Equations Lecture Notes in Computer Science (год публикации - 2019)
4.
Куликов А.С., Михайлин И.А., Мохов А., Подольский В.В.
Complexity of Linear Operators
Proceedings of the 30th International Symposium on Algorithms and Computation (ISAAC 2019) (год публикации - 2019)
10.4230/LIPIcs.ISAAC.2019.17
5.
Белова Т.А., Близнец И.А.
Algorithms for (n,3)-MAXSAT and parametrization above the-all true assignment
Theoretical Computer Science (год публикации - 2020)
10.1016/j.tcs.2019.11.033
6. Лялина А.А On the Complexity of Unique Circuit SAT Journal of Mathematical Sciences, Vol. 247, No. 3, 457-466 (год публикации - 2020)
7. Басс С, Ицыксон Д.М., Кноп А.А., Рязанов А.А., Соколов Д.О. Lower Bounds on OBDD Proofs with Several Orders Electronic Colloquium on Computational Complexity (год публикации - 2020)
8.
Головнёв А.Г., Куликов А.С., Вильямс Р.
Circuit Depth Reductions
Leibniz International Proceedings in Informatics (Proceedings of 12th Innovations in Theoretical Computer Science Conference), 12th Innovations in Theoretical Computer Science Conference (ITCS 2021) стр 24:1--24:20 том 185 (год публикации - 2021)
10.4230/LIPIcs.ITCS.2021.24
9. Алферов В., Близнец И New Length Dependent Algorithm for Maximum Satisfiability Problem Thirty-Fifth AAAI Conference on Artificial Intelligence (год публикации - 2021)
10. Ицыксон Д.М., Рязанов А.А. Dmitry Itsykson, Artur Riazanov. Proof complexity of natural formulas via communication arguments Leibniz International Proceedings in Informatics (Proceedings of Computational Complexity Conference) (год публикации - 2021)
11. Софронова А.А., Соколов Д.О. Branching Programs with Bounded Repetitions and Flow Formulas Leibniz International Proceedings in Informatics (Proceedings of Computational Complexity Conference) (год публикации - 2021)
Публикации
1. Лялина А. А. Верхняя оценка для задачи выполнимости булевых схем с единственным выполняющим набором Записки научных семинаров ПОМИ, т. 475, с. 122–137 (год публикации - 2018)
2.
Белова Т.С., Близнец И.А.
Upper and Lower Bounds for Different Parameterizations of (n,3)-MAXSAT
Lecture Notes in Computer Science, том 11346, с. 299–313 (год публикации - 2018)
10.1007/978-3-030-04651-4_20
3. Грязнов С. Notes on Resolution over Linear Equations Lecture Notes in Computer Science (год публикации - 2019)
4.
Куликов А.С., Михайлин И.А., Мохов А., Подольский В.В.
Complexity of Linear Operators
Proceedings of the 30th International Symposium on Algorithms and Computation (ISAAC 2019) (год публикации - 2019)
10.4230/LIPIcs.ISAAC.2019.17
5.
Белова Т.А., Близнец И.А.
Algorithms for (n,3)-MAXSAT and parametrization above the-all true assignment
Theoretical Computer Science (год публикации - 2020)
10.1016/j.tcs.2019.11.033
6. Лялина А.А On the Complexity of Unique Circuit SAT Journal of Mathematical Sciences, Vol. 247, No. 3, 457-466 (год публикации - 2020)
7. Басс С, Ицыксон Д.М., Кноп А.А., Рязанов А.А., Соколов Д.О. Lower Bounds on OBDD Proofs with Several Orders Electronic Colloquium on Computational Complexity (год публикации - 2020)
8.
Головнёв А.Г., Куликов А.С., Вильямс Р.
Circuit Depth Reductions
Leibniz International Proceedings in Informatics (Proceedings of 12th Innovations in Theoretical Computer Science Conference), 12th Innovations in Theoretical Computer Science Conference (ITCS 2021) стр 24:1--24:20 том 185 (год публикации - 2021)
10.4230/LIPIcs.ITCS.2021.24
9. Алферов В., Близнец И New Length Dependent Algorithm for Maximum Satisfiability Problem Thirty-Fifth AAAI Conference on Artificial Intelligence (год публикации - 2021)
10. Ицыксон Д.М., Рязанов А.А. Dmitry Itsykson, Artur Riazanov. Proof complexity of natural formulas via communication arguments Leibniz International Proceedings in Informatics (Proceedings of Computational Complexity Conference) (год публикации - 2021)
11. Софронова А.А., Соколов Д.О. Branching Programs with Bounded Repetitions and Flow Formulas Leibniz International Proceedings in Informatics (Proceedings of Computational Complexity Conference) (год публикации - 2021)