Страница публикации
О способах пропозиционального кодирования различимости объектов в конечных множествах
Авторы: Белей Е.Г., Семенов А.А.
Журнал: Известия Иркутского государственного университета. Сер. Математика
Том: 28
Номер:
Год: 2019
Отчётный год: 2019
Издательство:
Местоположение издательства:
URL:
Проекты:
DOI: 10.26516/1997-7670.2019.28.3
Аннотация: Для изучаемого в настоящей работе класса комбинаторных проблем достаточно представлять элементы рассматриваемого множества их натуральными номерами. Соответственно, возникает задача построения выполнимой булевой формулы, выполняющие наборы которой кодируют первые n целых неотрицательных чисел без учета их порядка. Необходимость булевого кодирования таких множеств вызвана желанием применить к соответствующим комбинаторным задачам алгоритмы решения проблемы булевой выполнимости (SAT). В статье предлагается новый способ задания булевой формулой характеристической функции предиката, который истин на наборе двоичных слов, представляющих числа от 0 до n - 1. Соответствующий предикат назван OtO (сокращение от One-to-One). Пропозициональная кодировка OtO-предиката имеет более экономную асимптотику роста в сравнении с кодировкой для близкого по смыслу предиката, известного как OOC-предикат (от Only One Cardinality). Описанный в статье OtO-предикат используется для сведения к SAT ряда задач, связанных с латинскими квадратами. Конкретно, с помощью OtO-предиката строятся SAT-кодировки для задач поиска ортогональных пар и квазиортогональных троек латинских квадратов порядка 10. Для вычислительного решения этих задач используются многопоточный SAT-решатель и вычислительный кластер.
Индексируется WOS: Нет
Индексируется Scopus: Нет
Индексируется УБС: Нет
Индексируется РИНЦ: Да
Индексируется ВАК: Нет
Индексируется CORE: Нет
Публикация в печати: 0