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

Using Disjunctive Diagrams for Preprocessing of Conjunctive Normal Forms

Авторы: Kondratiev V.

Журнал: 45th Jubilee International Convention on Information, Communication and Electronic Technology, MIPRO 2022

Том:

Номер:

Год: 2022

Отчётный год: 2022

Издательство:

Местоположение издательства:

URL:

Проекты:

Теоретические основы, методы и высокопроизводительные алгоритмы непрерывной и дискретной оптимизации для поддержки междисциплинарных научных исследований

DOI: 10.23919/MIPRO55190.2022.9803639

Аннотация: In this article, in the context of the Boolean satisfiability problem (SAT), the question of speeding up the SAT solvers on specific input formulas is considered. The speedup is achieved using the CNF preprocessing algorithm which is based on the use of decision diagrams of a special kind, called Disjunctive Diagrams. These diagrams allow one to naturally test some sets of partial variable assignments and add more stringent constraints to the original formula. Several families of SAT instances are considered and used to compare the solving time before and after preprocessing, including a selection of tests from the "SAT Competition 2021"and some tests related to the problem of checking the equivalence of Boolean circuits.Computational experiments have shown that for hard instances in more than half of the cases the proposed preprocessing algorithm can speed up the solving time of considered CNFs.

Индексируется WOS: Нет

Индексируется Scopus: Нет

Индексируется УБС: Нет

Индексируется РИНЦ: Нет

Индексируется ВАК: Нет

Индексируется CORE: Нет

Публикация в печати: 0