Разница между C-SAT и SAT?

В чем именно разница между этими двумя NP-полными задачами? Мне кажется, что они оба спрашивают, может ли быть выполнена булева формула (т.е. вывод 1), но один находится в контексте схемы, а другой - просто формула. Однако нельзя ли написать булеву формулу из булевой схемы?

2 ответа

Вы правы, они очень близки друг к другу. Любая проблема C-SAT может быть представлена ​​как SAT, любая проблема SAT может быть представлена ​​как C-SAT. Возникает вопрос, как наиболее эффективно перевести C-SAT <-> SAT. Некоторые задачи лучше представить в виде SAT, некоторые из них "выглядят" лучше как C-SAT.

Кроме того, существуют решатели SAT, которые используют представление схемы внутри, а не в более популярной клаузальной форме.

Далее вы можете прочитать этот замечательный обзор: М. Бьорк, 2009, Успешные методы кодирования SAT

Обе проблемы связаны с выполнимостью булевых функций. Разница заключается в способе представления функций — либо в виде схем, либо в виде формул.

В схеме выход одного вентиля может использоваться несколько раз. При переводе схемы в формулу очевидным способом решения этой проблемы является дублирование частей схемы, что может привести к экспоненциальному увеличению размера.

Другие вопросы по тегам