Страница публикации

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

Тип публикации: Статья в журнале

Тип материала: Текст

Авторы: Белей Е.Г., Семенов А.А.

Журнал: Известия Иркутского государственного университета. Сер. Математика

Язык публикации: russian

Том: 28

Номера страниц: 3-20

Количество страниц: 18

Год публикации: 2019

Отчетный год: 2019

Переводная версия: {"id":4934,"authors":"Beley E., Semenov A.","authors_count":2,"title":"On Propositional Encoding of Distinction Property in Finite Sets","journal":"Bulletin of Irkutsk State University-Series Mathematics","year":2019,"reportYear":2019,"volume":"28","number":"","month":null,"url":"","pages":"3-20","address":"","type":"\u0422\u0435\u043a\u0441\u0442","publisher":"","edition":"","language":"russian","classification":"\u0421\u0442\u0430\u0442\u044c\u0438 \u0432 \u0440\u043e\u0441\u0441\u0438\u0439\u0441\u043a\u0438\u0445 \u0436\u0443\u0440\u043d\u0430\u043b\u0430\u0445","annotation":"In the paper we describe a new propositional encoding procedure for the property that all objects comprising some finite set are distinct. For the considered class of combinatorial problems it is sufficient to represent the elements of such set by their natural numbers. Thus, there is a problem of constructing a satisfiable Boolean formula, the satisfying assignments of which encode the first n natural numbers without taking into account their order. The necessity to encode such sets into Boolean logic is motivated by the desire to apply to the corresponding combinatorial problems the state-of-the-art algorithms for solving the Boolean satisfiability problem (SAT). In the paper we propose the new approach to defining the Boolean formula for the characteristic function of the predicate which takes the value of True only on the sets of binary words encoding the numbers from 0 to n - 1. The corresponding predicate was named OtO (from One-to-One). The propositional encoding of the OtO-predicate has a better lower bound compared to the propositional encoding of a relatively similar predicate known as OOC-predicate (from Only One Cardinality). The proposed OtO-predicate is used to reduce to SAT a number of problems related to Latin squares. In particular, using the OtO-predicate we constructed the SAT encodings for the problems of finding orthogonal pairs and quasi-orthogonal triples of Latin squares of order 10. We used the multi-threaded SAT solvers and the resources of a computing cluster to solve these problems.","published_at":null,"doi":"10.26516\/1997-7670.2019.28.3","is_to_print":0,"is_special":0,"is_wos":1,"is_scopus":1,"is_risc":0,"is_editable":0,"publication_type_id":1,"added_by_rb_user_id":null,"notes":"","created_at":"2019-08-07 01:16:30","updated_at":"2019-11-05 10:11:19","translated_id":null,"quartile":"Q5","series":"","is_vak":0,"conference":null,"is_public_pdf":0,"eid":null,"wosid":null,"quartile_scopus":null,"report_type":null,"speaker":0,"is_wl":0,"quartile_wl":null,"count_pages":18,"date_event_start":null,"date_event_end":null,"location_event":null,"lvl_event":null,"link_event":null,"title_event":null,"is_affiliation_idstu":null,"is_expert_opinion":null,"quartile_vak":null,"id_author_reference":null,"is_cr":null,"quartile_cr":null,"registration_number":null}

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: Нет