Application of SAT-approach for solving combinatorial problems

In the report, we present results of applying symbolic computation algorithms to solving discrete automata research problems (e.g. problems of analysis of discrete models of gene networks) and combinatorial optimization problems. In all cases, an original problem is translated into Boolean equations (and after this to SAT) and then is solved using SAT-solver. Optimization problems are solved in distributed computing environments with the help of the SAT-solver specially developed for this task.