В работе рассматривается задача о раскраске графов специального вида, сведение этой задачи к задаче выполнимости булевых формул (SAT) и оптимизация параметров SAT-решателя, позволяющая решать задачи такого вида за меньшее время. Задача о существовании правильной раскраски графа G в k цветов, вообще говоря, является NP-полной при k >= 3, и может быть различными способами сведена к другой хорошо известной NP-полной задаче - задаче выполнимости булевых формул в конъюнктивной нормальной форме. От кодировки может зависеть эффективность работы SAT-решателей (специализированных программ для решения задачи выполнимости). Выполнялась оптимизация параметров SAT-решателя Glucose при помощи генетического алгоритма, реализованного в пакете PyDGGA. Оптимизация позволила ускорить работу Glucose в 3-5 раз.

SAT-решатели, раскраска графов

Свистунова Виктория Романовна,  Адыгейский Государственный Университет