Кочемазов С.Е.   Заикин О.С.   Семёнов А.А.  

Сравнение различных пропозициональных кодировок для задач поиска систем ортогональных латинских квадратов

Докладчик: Заикин О.С.

Сравнение различных пропозициональных кодировок для задач поиска систем ортогональных латинских квадратов

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

Латинским квадратом порядка n - это квадратная таблица n x n, заполненная элементами из множества {1,…,n} таким образом, что каждый элемент появляется в каждом столбце и каждой строке ровно один раз. Два латинских квадрата A и B называются ортогональными, если различны все пары вида (a_ij,b_ij ),a_ij \in A,b_ij \in B,i,j \in {1,…,n}. Одна из наиболее широко известных нерешенных комбинаторных задач состоит в том, чтобы ответить на вопрос о существовании тройки попарно ортогональных латинских квадратов порядка 10. В силу высокой сложности этой задачи, в современной литературе часто рассматриваются упрощенные ее постановки, например поиск таких троек латинских квадратов порядка 10, в которых первый квадрат ортогонален двум другим, а второй и третий ортогональны только относительно ограниченного числа ячеек.

В силу того, что проблема построения пар ортогональных латинских квадратов порядка 10 имеет высокую комбинаторную сложность, имеет смысл применять SAT-подход к построению систем такого рода. SAT-подход состоит в сведении оригинальной задачи к SAT и последующем применении к ее решению современных последовательных и параллельных алгоритмов решения SAT. Несмотря на то, что SAT является NP-полной задачей, многие практические проблемы из разных областей науки и промышленности можно эффективно решать при помощи SAT-подхода. Благодаря заметному прогрессу в отношении эффективности современных алгоритмов решения SAT в последние годы, спектр задач, к которым можно применять соответствующий подход, увеличивается с каждым годом.

Без ограничения общности, рассмотрим задачу поиска пар ортогональных латинских квадратов. Эта задача интересна тем, что мы можем сводить ее к SAT многими различными способами. Так, мы можем рассмотреть ее в постановке для родственных латинским квадратам комбинаторных структур. Например, пара ортогональных латинских квадратов может быть представлена в виде ортогонального массива или множества непересекающихся трансверсалей. Это значит, что мы можем осуществить сведение этой задачи к SAT как минимум тремя существенно отличающимися способами. Помимо этого, так как SAT рассматривается для булевой формулы над множеством булевых переменных, нам необходимо представлять элементы латинского квадрата или родственной комбинаторной структуры при помощи булевых переменных. Как правило, это делается при помощи одного из двух способов. Согласно первому из них, число от 1 до n представляется при помощи n булевых переменных. При использовании второго подхода мы рассматриваем двоичную кодировку этого числа и записываем ее при помощи \floor{log n} +1 булевых переменных. Пропозициональная кодировка задач поиска систем латинских квадратов использует большое количество ограничений вида At-Most-One (AMO) и At-Least-One (ALO). В зависимости от выбранного способа представления чисел эти ограничения могут быть закодированы в SAT при помощи ряда различных методов.

В результате проведенного исследования мы построили несколько различных вариантов пропозициональных кодировок для поиска систем ортогональных латинских квадратов порядка 10. Мы сравнили их по числу литералов и дизъюнктов в соответствующих булевых формулах, и оценили их эффективность при помощи современных параметризованных алгоритмов решения SAT.