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

Using Decision Diagrams of Special Kind for Compactification of Conflict Data Bases Generated by CDCL SAT Solvers

Авторы: Kondratiev V., Otpuschennikov I., Semenov A.

Журнал: Proceedings 43rd Intern. Convention on Information, Communication and Electronic Technology (MIPRO 2020; 28 September - 2 October 2020, Opatija, Croatia)

Том:

Номер:

Год: 2020

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

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

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

URL:

Проекты:

DOI: 10.23919/MIPRO48935.2020.9245180

Аннотация: In the paper we propose new algorithms for constructing compact representations of databases of conflict clauses accumulated by state-of-the-art CDCL SAT solvers. These algorithms use the Decision Diagrams of a special kind (the so-called Disjunctive Diagrams). We consider several families of hard SAT instances and use them to compare the implementations of the proposed algorithms and the well-known CUDD package that uses Zero-Suppressed Binary Decision Diagrams (ZBDD) for solving similar problems. The computational experiments clearly show that our algorithm that uses Disjunctive Diagrams has better effectiveness compared to CUDD.

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

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

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

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

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

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

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