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

В статье описана новая процедура пропозиционального кодирования свойства различимости объектов, составляющих некоторое конечное множество. Для изучаемого в настоящей работе класса комбинаторных проблем достаточно представлять элементы рассматриваемого множества их натуральными номерами. Соответственно, возникает задача построения выполнимой булевой формулы, выполняющие наборы которой кодируют первые $n$ целых неотрицательных чисел без учета их порядка. Необходимость булевого кодирования таких множеств вызвана желанием применить к соответствующим комбинаторным задачам алгоритмы решения проблемы булевой выполнимости (SAT). В статье предлагается новый способ задания булевой формулой характеристической функции предиката, который истин на наборе двоичных слов, представляющих числа от $0$ до $n-1$. Соответствующий предикат назван OtO (сокращение от One-to-One). Пропозициональная кодировка OtO-предиката имеет более экономную асимптотику роста в сравнении с кодировкой для близкого по смыслу предиката, известного как OOC-предикат (от Only One Cardinality). Описанный в статье OtO-предикат используется для сведения к SAT ряда задач, связанных с латинскими квадратами. Конкретно, с помощью OtO-предиката строятся SAT-кодировки для задач поиска ортогональных пар и квазиортогональных троек латинских квадратов порядка $10$. Для вычислительного решения этих задач используются многопоточный SAT-решатель и вычислительный кластер.