Экзистенциальная теория вещественных чисел

Экзистенциальная теория вещественных чисел — это множество всех верных утверждений вида

${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),\,}$

где ${\displaystyle F(X_{1},\dots X_{n})}$ — это формула без кванторов^[англ.], в которую входят равенства и неравенства вещественных многочленов^[1].

Задача разрешимости для экзистенциальной теории вещественных чисел — это задача нахождения алгоритма, который решает для каждой формулы, верна она или нет. Эквивалентно, это задача проверки, что заданное полуалгебраическое множество не пусто^[1]. Эта задача разрешимости является NP-трудной и лежит в PSPACE^[2]. Таким образом, задача имеет существенно меньшую сложность, чем процедура исключения кванторов Альфреда Тарского в теориях первого порядка вещественных^[1]. Однако, на практике, общие методы для теории первого порядка остаются предпочтительным выбором для решения такого рода задач^[3].

Многие естественные задачи геометрической теории графов^[англ.], особенно задачи распознавания геометрических графов пересечений и выпрямления рёбер рисунков графов с пересечениями, могут быть решены путём преобразования их в вариант экзистенциальной теории вещественных чисел и являются полными^[англ.] для этой теории. Для описания этих задач определяется класс сложности ${\displaystyle \exists \mathbb {R} }$, находящийся между NP и PSPACE ^[4].

Предпосылки

В математической логике «теория» — это формальный язык, состоящий из множества предложений, записанных с использованием фиксированного набора символов. Теория первого порядка вещественно замкнутых полей^[англ.] имеет следующие символы^[5]:

• константы 0 и 1,
• счётный набор переменных ${\displaystyle X_{i}}$,
• операции сложения, вычитания, умножения и (не обязательно) деления,
• символы <, ≤, =, ≥, > и ≠ для сравнения вещественных значений,
• логические операции ∧, ∨, ¬ и ⇔,
• скобки
• квантор всеобщности ∀ и квантор существования ∃

Последовательность этих символов образует предложение, которое принадлежат теории первого порядка вещественных чисел, если грамматически правильно построено, все его переменные имеют соответствующие кванторы и (когда интерпретируется как математическое утверждение о вещественных числах) является верным утверждением. Как показал Тарский, эта теория может быть описана схемой аксиом и процедурой принятия решений, которая является полной и эффективной, это: для любого грамматически верного утверждения с полным набором кванторов либо само утверждение, либо его отрицание (но не оба) может быть выведено из аксиом. Та же самая теория описывает любое вещественно замкнутое поле^[англ.]*, не просто вещественные числа^[6]. Существуют, однако, другие числовые системы, которые не описываются этими аксиомами точно. Теория, определённая тем же образом для целых чисел вместо вещественных чисел, согласно теореме Матиясевича, является неразрешимой даже для утверждений существования для диофантовых уравнений^[5][7].

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

${\displaystyle \exists X_{1}\cdots \exists X_{n}\,F(X_{1},\dots ,X_{n}),\,}$

где ${\displaystyle F(X_{1},\dots X_{n})}$ — формула без кванторов^[англ.], содержащая равенства и неравенства с многочленами над вещественными числами. Задача разрешимости для экзистенциальной теории вещественных чисел — это алгоритмическая задача проверки, принадлежит ли данное предложение этой теории. Эквивалентно, для строк, проходящих базовые синтаксические проверки (то есть предложение использует правильные символы, имеет правильный синтаксис и не имеет переменных без кванторов), является задачей проверки, что утверждение является верным утверждением над вещественными числами. Множество n-кортежей вещественных чисел ${\displaystyle (X_{1},\dots X_{n})}$, для которых ${\displaystyle F(X_{1},\dots X_{n})}$ верно, называется полуалгебраическое множество, так что задача разрешимости для экзистенциальной теории вещественных чисел может эквивалентно быть перефразирована как проверка, что заданное полуалгебраическое множество не пусто^[1].

Для определения временно́й сложности алгоритмов для задачи разрешимости экзистенциальной теории вещественных чисел важно иметь способ измерения размера входа. Простейший способ измерения этого типа – длина предложения, то есть число символов, входящих в утверждение^[5]. Однако, чтобы получить более точный анализ поведения алгоритмов для этой задачи, удобно разбить размер входа на несколько переменных, выделяя число переменных с кванторами, число многочленов в предложении и степени этих многочленов^[8].

Примеры

Золотое сечение ${\displaystyle \varphi }$ можно определить как корень многочлена ${\displaystyle x^{2}-x-1}$. Этот многочлен имеет два корня, из которых только один (золотое сечение) превосходит единицу. Таким образом, существование золотого сечения можно выразить предложением

${\displaystyle \exists X_{1}(X_{1}>1\wedge X_{1}\times X_{1}-X_{1}-1=0).}$

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

Неравенство между средним арифметическим и средним геометрическим утверждает, что для любых двух неотрицательных чисел ${\displaystyle x}$ и ${\displaystyle y}$ выполняется следующее неравенство:

${\displaystyle {\frac {x+y}{2}}\geq {\sqrt {xy}}.}$

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

${\displaystyle \exists X_{1}\exists X_{2}{\bigl (}X_{1}\geq 0\wedge X_{2}\geq 0\wedge (X_{1}+X_{2})\times (X_{1}+X_{2})<(1+1+1+1)\times X_{1}\times X_{2}{\bigr )}.}$

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

Алгоритмы

Метод Альфреда Тарского исключения кванторов (1948) показывает, что экзистенциальная теория вещественных чисел (и, более обще, теория первого порядка вещественных чисел) алгоритмически разрешимы, но без элементарных границ на сложность^[9][6]. Метод цилиндрической алгебраической декомпозиции Коллинза^[англ.] (1975) улучшил зависимость от времени до двойной экспоненциальности^[9],^[10] вида

${\displaystyle L^{3}(md)^{2^{O(n)}}}$

где ${\displaystyle L}$ — число бит, требуемых для представления коэффициентов в утверждении, значение которого требуется определить, ${\displaystyle m}$ — число многочленов в утверждении, ${\displaystyle d}$ — их общая степень, а ${\displaystyle n}$ — число переменных ^[8] В 1988 Дмитрий Григорьев^[англ.] и Николай Воробьёв показали, что сложность экспоненциальна со степенью, являющейся многочленом от ${\displaystyle n}$^[8][11][12],

${\displaystyle L(md)^{n^{2}}}$

и в последовательности статей, опубликованных в 1992, Джеймс Ренегар улучшил оценку до слегка превышающей экспоненту on ${\displaystyle n}$^{[8][13][14][15]}.

${\displaystyle L\log L\log \log L(md)^{O(n)}.}$

Между тем, в 1988 Джон Кэнни^[англ.] описал другой алгоритм, который также экспоненциально зависит по времени, но имеет лишь полиномиальную сложность по памяти. То есть он показал, что задача может быть решена в классе PSPACE^[2][9].

Асимптотическая вычислительная сложность^[англ.] этих алгоритмов может ввести в заблуждение, поскольку алгоритмы могут работать с входом только очень малого размера. Сравнивая в 1991 алгоритмы, Хун Хонг оценил время работы процедуры Коллинза (с двойной экспоненциальной оценкой) для задачи, размер которой описывается установкой всех приведённых выше параметров в 2, в менее чем две секунды, в то время как алгоритмы Григорьева, Воробьёва и Ренегара потратили бы на решение задачи более миллиона лет^[8]. В 1993 Йос, Рой и Солерно высказали предположение, что должна существовать возможность небольшой модификации процедур с экспоненциальным временем, чтобы сделать их на практике быстрее цилиндрического алгебраического решения, что соответствовало бы теории^[16]. Однако, на момент 2009, общие методы для теории первого порядка вещественных чисел остаются лучшими на практике по сравнению с алгоритмами с простой экспоненциальной оценкой, специально разработанными для экзистенциальной теории вещественных чисел^[3].

Полные задачи

Некоторые задачи вычислительной сложности и геометрической теории графов^[англ.] могут быть классифицированы как полные^[англ.] для экзистенциальной теории вещественных чисел. То есть любая задача из экзистенциальной теории вещественных чисел имеет полиномиальное многозначное сведение к варианту одной из этих задач и, наоборот, эти задачи сводимы к экзистенциальной теории вещественных чисел^[4][17].

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

• распознавание графов пересечений отрезков на плоскости^[4][18][5],
• распознавание графов единичных кругов^[19]
• распознавание графов пересечений выпуклых множеств на плоскости^[4].

Для графов, нарисованных на плоскости без пересечений, теорема Фари утверждает, что мы получим тот же класс планарных графов независимо от того, должны ли рёбра графа быть нарисованы в виде отрезков, либо их можно рисовать в виде кривых. Но эта эквивалентность классов не верна для других типов вычерчивания графов. Например, хотя число пересечений графа (минимальное число пересечений рёбер при криволинейных рёбрах) может быть определено как принадлежащее классу NP, для экзистенциальной теории вещественных чисел задача определения, существуют ли рисунки, на которых достигается заданная граница прямолинейного числа пересечений (минимальное число пар рёбер, которые пересекаются в любом рисунке с рёбрами в виде прямолинейных отрезков на плоскости), является полной^[4][20]. Полной также является для экзистенциальной теории вещественных чисел задача проверки, можно ли данный граф нарисовать на плоскости с отрезками в виде прямолинейных рёбер и с заданным множеством пар пересекающихся рёбер или, эквивалентно, можно ли рисунок с криволинейными рёбрами с пересечениями выпрямить таким образом, что пересечения сохранятся^[21].

Другие полные задачи для экзистенциальной теории вещественных чисел:

• задача о картинной галерее заключается в поиске наименьшего числа точек, из которых видны все точки заданного многоугольника^[22].
• распознавание графов единичных графов и проверка, не превосходит ли размерность или евклидова размерность графа заданного значения^[9].
• выпрямление псевдопрямых (то есть, если дано семейство кривых на плоскости, определение, гомеоморфны ли они конфигурации прямых)^[4][23][24];
• слабая и сильная выполнимость геометрической квантовой логики в любой фиксированной размерности >2^[25];
• алгоритмическая задача Штайница (дана решётка, определить, является ли она решёткой грани выпуклого многогранника), даже если ограничиться четырёхмерными многогранниками^[26][27];
• реализация пространств размещения некоторых выпуклых тел^[28].
• различные свойства равновесия Нэша игр нескольких лиц^[29][30]

^[31];

• вложение заданного абстрактного комплекса треугольников и четырёхугольников в трёхмерное евклидово пространство^[17];
• вложение нескольких графов на общем множестве вершин в плоскость так, что все графы будут нарисованы без пересечений^[17];
• распознавание графов видимости плоских множеств точек^[17];
• (проективная или нетривиальная аффинная) выполнимость равенства двух векторных произведений^[32];
• определение минимального числа наклонов рисунка без пересечений рёбер планарного графа^[33].

Опираясь на это, класс сложности ${\displaystyle \exists \mathbb {R} }$ определяется как множество задач, имеющих полиномиальное время сведения по Карпу к экзистенциальной теории вещественных чисел^[4].

Примечания

1. Basu, Pollack, Roy, 2006, с. 505–532.
2. Canny, 1988, с. 460–467.
3. Passmore, Jackson, 2009, с. 122–137.
4. Schaefer, 2010, с. 334–344.
5. Matoušek, 2014.
6. Tarski, 1948.
7. Matiyasevich, 2006, с. 185–213.
8. Hong, 1991.
9. Schaefer, 2013, с. 461–482.
10. Collins, 1975, с. 134–183.
11. Grigor'ev, 1988, с. 65–108.
12. Grigor'ev, Vorobjov, 1988, с. 37–64.
13. Renegar, 1992, с. 255–299.
14. Renegar, 1992, с. 301–327.
15. Renegar, 1992, с. 329–352.
16. Heintz, Roy, Solernó, 1993, с. 427–431.
17. Cardinal, 2015, с. 69–78.
18. Kratochvíl, Matoušek, 1994, с. 289–315.
19. Kang, Müller, 2011, с. 308–314.
20. Bienstock, 1991, с. 443–459.
21. Kynčl, 2011, с. 383–399.
22. Abrahamsen, Adamaszek, Miltzow, 2017.
23. Mnëv, 1988, с. 527–543.
24. Shor, 1991, с. 531–554.
25. Herrmann, Ziegler, 2016.
26. Björner, Las Vergnas, Sturmfels, White, Ziegler, 1993.
27. Richter-Gebert, Ziegler, 1995, с. 403–412.
28. Dobbins, Holmsen, Hubard, 2014.
29. Garg, Mehta, Vazirani, Yazdanbod, 2015, с. 554–566.
30. Bilo, Mavronicolas, 2016, с. 17:1–17:13.
31. Bilo, Mavronicolas, 2017, с. 13:1–13:14.
32. Herrmann, Sokoli, Ziegler, 2013.
33. Hoffmann, 2016.

Литература

• Saugata Basu, Richard Pollack, Marie-Françoise Roy. Existential theory of the reals // Algorithms in Real Algebraic Geometry. — 2. — Springer-Verlag, 2006. — Т. 10. — С. 505–532. — (Algorithms and Computation in Mathematics). — ISBN 978-3-540-33098-1. — doi:10.1007/3-540-33099-2_14.
• John Canny. Some algebraic and geometric computations in PSPACE // Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing (STOC '88, Chicago, Illinois, USA). — New York, NY, USA: ACM, 1988. — С. 460–467. — ISBN 0-89791-264-0. — doi:10.1145/62212.62257.
• Matiyasevich Yu. V. Hilbert's tenth problem: Diophantine equations in the twentieth century // Mathematical events of the twentieth century. — Berlin: Springer-Verlag, 2006. — С. 185–213. — doi:10.1007/3-540-29462-7_10.
• Alfred Tarski. A Decision Method for Elementary Algebra and Geometry. — RAND Corporation, Santa Monica, Calif., 1948.
• George E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition // Automata theory and formal languages (Second GI Conf., Kaiserslautern, 1975). — Berlin: Springer-Verlag, 1975. — Т. 33. — С. 134–183. — (Lecture Notes in Computer Science).
• Hoon Hong. Comparison of Several Decision Algorithms for the Existential Theory of the Reals. — RISC Linz, 1991. — Т. 91-41. — (Technical Report). (недоступная ссылка)
• Grigor'ev D. Yu. Complexity of deciding Tarski algebra // Journal of Symbolic Computation. — 1988. — Т. 5, вып. 1—2. — С. 65—108. — doi:10.1016/S0747-7171(88)80006-3.
• Grigor'ev D. Yu., Vorobjov N. N. Jr. Solving systems of polynomial inequalities in subexponential time // Journal of Symbolic Computation. — 1988. — Т. 5, вып. 1—2. — С. 37—64. — doi:10.1016/S0747-7171(88)80005-1.
• James Renegar. On the computational complexity and geometry of the first-order theory of the reals. I. Introduction. Preliminaries. The geometry of semi-algebraic sets. The decision problem for the existential theory of the reals // Journal of Symbolic Computation. — 1992. — Т. 13, вып. 3. — С. 255—299. — doi:10.1016/S0747-7171(10)80003-3.
• James Renegar. On the computational complexity and geometry of the first-order theory of the reals. II. The general decision problem. Preliminaries for quantifier elimination // Journal of Symbolic Computation. — 1992. — Т. 13, вып. 3. — С. 301—327. — doi:10.1016/S0747-7171(10)80004-5.
• James Renegar. On the computational complexity and geometry of the first-order theory of the reals. III. Quantifier elimination // Journal of Symbolic Computation. — 1992. — Т. 13, вып. 3. — С. 329—352. — doi:10.1016/S0747-7171(10)80005-7.
• Joos Heintz, Marie-Françoise Roy, Pablo Solernó. On the theoretical and practical complexity of the existential theory of reals // The Computer Journal. — 1993. — Т. 36, вып. 5. — С. 427—431. — doi:10.1093/comjnl/36.5.427.
• Grant Olney Passmore, Paul B. Jackson. Intelligent Computer Mathematics: 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009, Proceedings, Part II. — Springer-Verlag, 2009. — Т. 5625. — С. 122—137. — doi:10.1007/978-3-642-02614-0_14.
• Jan Kratochvíl, Jiří Matoušek. Intersection graphs of segments // Journal of Combinatorial Theory. — 1994. — Т. 62, вып. 2. — С. 289—315. — doi:10.1006/jctb.1994.1071.
• Jiří Matoušek. Intersection graphs of segments and ${\displaystyle \exists \mathbb {R} }$. — 2014. — arXiv:1406.2636.
• Ross J. Kang, Tobias Müller. Sphere and dot product representations of graphs // Proceedings of the Twenty-Seventh Annual Symposium on Computational Geometry (SCG'11), June 13–15, 2011, Paris, France. — 2011. — С. 308–314.
• Daniel Bienstock. Some provably hard crossing number problems // Discrete and Computational Geometry. — 1991. — Т. 6, вып. 5. — С. 443—459. — doi:10.1007/BF02574701.
• Jan Kynčl. Simple realizability of complete abstract topological graphs in P // Discrete and Computational Geometry. — 2011. — Т. 45, вып. 3. — С. 383—399. — doi:10.1007/s00454-010-9320-x.
• Mikkel Abrahamsen, Anna Adamaszek, Tillmann Miltzow. The Art Gallery Problem is ${\displaystyle \exists \mathbb {R} }$-complete. — 2017. — arXiv:1704.06969.
• Marcus Schaefer. Realizability of graphs and linkages // Thirty Essays on Geometric Graph Theory / János Pach. — Springer-Verlag, 2013. — С. 461–482. — doi:10.1007/978-1-4614-0110-0_24.
• Mnëv N. E. The universality theorems on the classification problem of configuration varieties and convex polytopes varieties // Topology and geometry—Rohlin Seminar. — Berlin: Springer-Verlag, 1988. — Т. 1346. — С. 527–543. — (Lecture Notes in Mathematics). — doi:10.1007/BFb0082792.
• Peter W. Shor. Stretchability of pseudolines is NP-hard // Applied Geometry and Discrete Mathematics. — Providence, RI: American Mathematical Society, 1991. — Т. 4. — С. 531–554. — (DIMACS Series in Discrete Mathematics and Theoretical Computer Science).
• Christian Herrmann, Martin Ziegler. Computational Complexity of Quantum Satisfiability // Journal of the ACM. — 2016. — Т. 63, вып. 19. — doi:10.1145/2869073.
• Anders Björner, Michel Las Vergnas, Bernd Sturmfels, Neil White, Günter M. Ziegler. Oriented Matroids. — Cambridge: Cambridge University Press, 1993. — Т. 46. — С. 407 Corollary 9.5.10. — (Encyclopedia of Mathematics and its Applications). — ISBN 0-521-41836-4.
• Jürgen Richter-Gebert, Günter M. Ziegler. Realization spaces of 4-polytopes are universal. — Bulletin of the American Mathematical Society. — 1995. — Т. 32. — С. 403–412. — (New Series). — doi:10.1090/S0273-0979-1995-00604-X.
• Michael Gene Dobbins, Andreas Holmsen, Alfredo Hubard. Realization spaces of arrangements of convex bodies. — 2014.
• Jugal Garg, Ruta Mehta, Vijay V. Vazirani, Sadra Yazdanbod. ETR-Completeness for Decision Versions of Multi-player (Symmetric) Nash Equilibria // Proc. 42nd International Colloquium on Automata, Languages, and Programming (ICALP). — Springer, 2015. — Т. 9134. — С. 554–566. — (Lecture Notes in Computer Science). — doi:10.1007/978-3-662-47672-7_45.
• Vittorio Bilo, Marios Mavronicolas. A Catalog of ETR-Complete Decision Problems about Nash Equilibria in Multi-Player Games // Proceedings of 33rd International Symposium on Theoretical Aspects of Computer Science. — Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik, 2016. — С. 17:1–17:13. — (LIPIcs). — doi:10.4230/LIPIcs.STACS.2016.17.
• Vittorio Bilo, Marios Mavronicolas. ETR-Complete Decision Problems about Symmetric Nash Equilibria in Symmetric Multi-Player Games // Proceedings of 34th International Symposium on Theoretical Aspects of Computer Science. — Schloss Dagstuhl--Leibnitz Zentrum fuer Informatik, 2017. — С. 13:1–13:14. — (LIPIcs).
• Christian Herrmann, Johanna Sokoli, Martin Ziegler. Satisfiability of cross product terms is complete for real nondeterministic polytime Blum-Shub-Smale machines // Proceedings of the 6th Conference on Machines, Computations and Universality (MCU'13). — 2013. — doi:10.4204/EPTCS.128.
• Udo Hoffmann. The planar slope number // Proceedings of the 28th Canadian Conference on Computational Geometry (CCCG 2016). — 2016.
• Marcus Schaefer. Complexity of some geometric and topological problems // Graph Drawing, 17th International Symposium, GD 2009, Chicago, IL, USA, September 2009, Revised Papers^[англ.]. — Springer-Verlag, 2010. — Т. 5849. — С. 334–344. — (Lecture Notes in Computer Science). — doi:10.1007/978-3-642-11805-0_32.
• Jean Cardinal. Computational geometry column 62 // SIGACT News. — 2015. — Декабрь (т. 46, вып. 4). — С. 69—78. — doi:10.1145/2852040.2852053.