On the complexity of unique Circuit SAT

В данной статье рассматривается задача выполнимости булевых схем с не более чем одним выполняющим набором. Приводится алгоритм, решающий эту задачу за время $O(2^{.374589m})$, где $m$ обозначает число внутренних гейтов схемы. Для полноты изложения в статье также описан полученный Савиновым алгоритм, который решает общую задачу выполнимости булевой схемы за время $O(2^{.389667m})$. Библ. — 13 назв.