As a result of the seminars conducted by the head of the Optimization problems in software engineering Group Vladimir Ulyantsev at the University of Lisbon in October 2016, a joint research project on methods for solving the problem of constructing minimal finite deterministic automata was started. Under remote cooperation research in this area had been carried out for several months, as well as software implementation of the developed methods and their experimental verification.
In the course of the work, an article reflecting the results of the research was written and will be sent to the A-level 20th International Conference on Theory and Applications of Satisfiability Testing (SAT2017).
The researcher of our Group Ilya Zakirzyanov, who deals with this topic, was sent to Lisbon for 15 days for the most effective interaction and with the aim of making the final breakthrough in this study. As a result of this trip, methods were developed and implemented for a more compact representation of the problem of constructing a minimal finite determinate automaton in the language of the satisfiability problem of Boolean formulas (SAT). Also, experimental studies of all developed methods were carried out, and an abstract of the article was prepared and sent to SAT2017. In the coming week, this article will be finalized and submitted to the conference.