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

Alias: a modular tool for finding backdoors for sat

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

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

Авторы: Kochemazov S., Zaikin O.

Журнал: Lecture Notes in Computer Science

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

Том: 10929 LNCS

Номера страниц: 419-427

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

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

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

DOI: 10.1007/978-3-319-94144-8_25

Аннотация: We present ALIAS, a modular tool aimed at finding backdoors for hard SAT instances. Here by a backdoor for a specific SAT solver and SAT formula we mean a set of its variables, all possible instantiations of which lead to construction of a family of subformulas with the total solving time less than that for an original formula. For a particular backdoor, the tool uses the Monte-Carlo algorithm to estimate the runtime of a solver when partitioning an original problem via said backdoor. Thus, the problem of finding a backdoor is viewed as a black-box optimization problem. The tool’s modular structure allows to employ state-of-the-art SAT solvers and black-box optimization heuristics. In practice, for a number of hard SAT instances, the tool made it possible to solve them much faster than using state-of-the-art multithreaded SAT-solvers.

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

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

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

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

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

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