Заметка об автоматическом решении квадратичных уравнений в словах
Автор: Непейвода Антонина Николаевна
Журнал: Программные системы: теория и приложения @programmnye-sistemy
Рубрика: Математические основы программирования
Статья в выпуске: 2 (37) т.9, 2018 года.
Бесплатный доступ
При анализе программ, оперирующих строками, естественным образом возникает задача решения уравнений в словах. На практике часто встречаются такие уравнения, содержащие, самое большее, два вхождения каждой переменной, –- так называемые квадратичные уравнения. Для их решения Ю. И. Хмелевским в 1971 году предложен интуитивно ясный алгоритм, имеющий экспоненциальную сложность. В 1999 году В. Дьекертом показано, что задача решения квадратичного уравнения является NP-трудной. В данной заметке изложены и показаны на примерах способы упрощения классического алгоритма Хмелевского, позволяющие добиться лучшей его применимости в автоматическом анализе программ.
Суперкомпиляция, уравнения в словах, анализ программ
Короткий адрес: https://sciup.org/143164301
IDR: 143164301 | УДК: 510.52 | DOI: 10.25209/2079-3316-2017-9-2-3-21
On solving quadratic word equations
Word equations are natural constraints in an automatic analysis of string manipulating programs. In particular, equations with at most two occurrences of each variable (quadratic word equations) are of interest of the analysis. The algorithm solving such equations with the exponential complexity is given by Yu. Hmelevskij in 1971. V. Diekert in 1999 proved that the satisfiability problem for the quadratic word equations is NP-hard. In this paper we suggest some refinements of Hmelevskij's algorithm to make it more applicable in the automatic analysis of programs. We consider the length analysis and splitting procedures and show when these refinements can be used to extract explicit solutions of the equations and when they can be used only for deciding satisfiability. (In Russian). (in Russian).
Список литературы Заметка об автоматическом решении квадратичных уравнений в словах
- А. П. Немытых. Суперкомпилятор SCP4: Общая структура, УРСС, М., 2007.
- N. Bjorner, N. Tillmann, A. Voronkov. "Path feasibility analysis for string-manipulating programs", Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2009, Lecture Notes in Computer Science, vol. 5505, eds. Kowalewski S., Philippou A., Springer, Berlin. P. 307-321.
- M. T. Trinh, D. H. Chu, J. Jaffar. "Progressive reasoning over recursively-defined strings", Computer Aided Verification, CAV 2016, Lecture Notes in Computer Science, vol. 9779, eds. Chaudhuri S., Farzan A., Springer, 2016. P. 218-240.
- F. Yu, T. Bultan, O. H. Ibarra. "Relational string verification using multi-track automata", Implementation and Application of Automata, CIAA 2010, Lecture Notes in Computer Science, vol. 6482, eds. Domaratzki M., Salomaa K., Springer, 2010. P. 290-299.
- T. Liang, A. Reynolds, N. Tsiskaridze, C. Tinelli, C. Barrett, M. Deters. "An efficient SMT solver for string constraints", Formal Methods in System Design, V. 48. No. 3. 2016. P. 206-234.
- J. Karhumaki, W. Plandowski, F. Mignosi. "The expressibility of languages and relations by word equations", Automata, Languages and Programming, ICALP 1997, Lecture Notes in Computer Science, vol. 1256, eds. Degano P., Gorrieri R., Marchetti-Spaccamela A., Springer, 1997. P. 98-109.
- J. Karhumaki, H. Maurer, G. Paun, G. Rozenberg (eds.). Jewels are forever. Contributions on theoretical computer science in honor of Arto Salomaa, Springer, 1999, 379 p.
- Ю. И. Хмелевский. Уравнения в свободной полугруппе//Тр. МИАН СССР, т. 107, 1971. С. 3-288.
- Г. С. Маканин. Проблема разрешимости уравнений в свободной полугруппе//Матем. сб., 103(145):2(6) 1977. С. 147-236.
- С. А. Романенко. Прогонка для программ на Рефале-4, Препринт № 211, Институт Прикладной Математики им. М. В. Келдыша АН СССР, 1987, 23 с.
- J. Karhumaki. Combinatorics of words.
- M. Huova. Combinatorics of words. New aspects on avoidability, defect effect, equations and palindromes, Ph.D. Thesis, Turku Centre for Computer Science, 2014, 140 p.
- M. H. Sørensen. Turchin's supercompiler revisited, Ms. Thesis, Department of Computer Science, University of Copenhagen, 1994, 143 p.
- A. Jez. "Recompression: a simple and powerful technique for word equations", J. ACM, V. 63. No. 1. (March 2016), 4, 51 p.
- С. М. Абрамов, А. Ю. Орлов. Компиляция в императивные языки синтаксического отождествления языка Рефал//Труды международной конференции "Программные системы: теория и приложения". Т. 1 (ИПС РАН, г. Переславль-Залесский, май 2004), ред. С. М. Абрамов, Физматлит, М., 2004. С. 403-448.
