Сложность пропозициональных доказательств

Сложность пропозициональных доказательств

Любую ли тавтологию в логике высказываний можно коротко (полиномиально от ее длины) доказать? Если такой системы доказательств нет, то классы сложности NP и coNP различаются и, в частности, различаются классы сложности P и NP. Основная программа исследований в теории сложности доказательств заключается в доказательстве суперполиномиальных нижних оценок для как можно более мощных систем доказательств. Теория сложности доказательств активно развивается более тридцати лет, предложен ряд общих методов, позволяющих доказывать нижние оценки для ряда систем доказательств, однако для многих интересных систем доказательств неизвестно нетривиальных нижних оценок (системы Фреге, полуалгебраические системы и пр.).

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

 

Сотрудники кафедры: 

Э.А.Гирш, Д.М.Ицыксон, А.А.Кноп, Д.О.Соколов

 

Публикации сотрудников кафедры

  1. M. Alekhnovich, E. A. Hirsch, D. Itsykson, Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas. Journal of Automated Reasoning (2005) 35: 51-72.
  2. D. Grigoriev, E. A. Hirsch, Algebraic proof systems over formulas. TCS 303/1: 83-102, 2003.
  3. D. Grigoriev, E. A. Hirsch, D. V. Pasechnik, Complexity of semialgebraic proofs. Moscow Mathematical Journal 2(4): 647-679, 2002.
  4. E. A. Hirsch, Optimal acceptors and optimal proof systems. Proceedings of TAMC-2010.
  5. E. A. Hirsch, D. Itsykson, I. Monakhov, A. Smal. On optimal heuristic randomized semidecision procedures, with applications to proof complexity and cryptography. Theory of Computing Systems 51(2):179-195, 2012.
  6. D. Itsykson, V. Oparin, M. Slabodkin, D. Sokolov. Tight Lower Bounds on the Resolution Complexity of Perfect Matching Principles, Fundamenta Informaticae, vol. 145, no. 3, pp. 229-242, 2016.
  7. D. Itsykson, D. Sokolov. Lower Bounds for Splittings by Linear Combinations. Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014. Proceedings Part II, pp. 372--383.
  8. D. Itsykson, D. Sokolov. On fast non-deterministic algorithms and short heuristic proofs. Fundamenta Informaticae, 132(1):113-129, 2014.
  9. D. Itsykson, D. Sokolov. The complexity of inversion of explicit Goldreich’s function by DPLL algorithms. Journal of Mathematical Sciences, 399:88-109, 2012.
  10. D. Itsykson, D. Sokolov. Lower bounds for myopic DPLL algorithms with a cut heuristic. Proceedings of the 22nd international conference on Algorithms and Computation, ISAAC'11, pp. 464 - 473, doi: 10.1007/978-3-642-25591-5_48.
  11. D. Itsykson, V. Oparin. Graph expansion, Tseitin formulas and resolution proofs for CSP. In proceedings of CSR 2013, LNCS 7913: 162-173
  12. D. Itsykson, Lower bound on average-case complexity of inversion of Goldreich function by "drunken" backtracking algorithms. In proceedings of CSR 2010, LNCS 6072, pp. 204-215.
  13. D. Itsykson, A. Kojevnikov, Lower bounds of static Lovasz-Schrijver calculus proofs for Tseitin tautologies. Journal of Mathematical Sciences 145(3):4942-4952, 2007.
  14. E. A. Hirsch, A. Kojevnikov, A. Kulikov, S. Nikolenko, Complexity of Semialgebraic Proofs with Restricted Degree of Falsity. Journal on Satisfiability, Boolean Modeling and Computation, Volume 6 (2008), pp. 53-69.
  15. E. A. Hirsch, A. Kojevnikov, Several notes on the power of Gomory-Chvátal cuts. Annals of Pure and Applied Logic 141(3):429-436, 2006.
  16. D. Itsykson, A. Okhotin, V. Oparin, Computational and Proof Complexity of Partial String Avoidability. 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016), pp. 51:1-51:13.

Квалификационные работы

  1. Э. А. Гирш. Сложность пропозициональной логики. Диссертация на соискание степени д.ф.-м.н. ПОМИ РАН, 2011.
  2. В. В. Опарин. Нижние оценки для алгоритмов расщепления. Магистерская диссертация, СПбАУ РАН, 2012.
  3. М. Г. Слабодкин. Нижние оценки на размер OBDD для линейных систем над полем F2. Магистерская диссертация, СПбАУ РАН, 2015.
  4. Д. О. Соколов Трудные примеры для эвристических DPLL алгоритмов для SAT. Магистерская диссертация, СПбАУ РАН, 2011.
  5. Д. О. Соколов. Нижние оценки на время обращения функции Голдрейха близорукими DPLL алгоритмами. Магистерская диссертация, СПбНИУ ИТМО, 2011.
  6. Д. О. Соколов. Сложность решения задачи выполнимости булевых формул алгоритмами, основанными на расщеплении. Диссертация на соискание степени к.ф.-м.н. ПОМИ РАН, 2015.