Разница между C-SAT и SAT?
В чем именно разница между этими двумя NP-полными задачами? Мне кажется, что они оба спрашивают, может ли быть выполнена булева формула (т.е. вывод 1), но один находится в контексте схемы, а другой - просто формула. Однако нельзя ли написать булеву формулу из булевой схемы?
2 ответа
Вы правы, они очень близки друг к другу. Любая проблема C-SAT может быть представлена как SAT, любая проблема SAT может быть представлена как C-SAT. Возникает вопрос, как наиболее эффективно перевести C-SAT <-> SAT. Некоторые задачи лучше представить в виде SAT, некоторые из них "выглядят" лучше как C-SAT.
Кроме того, существуют решатели SAT, которые используют представление схемы внутри, а не в более популярной клаузальной форме.
Далее вы можете прочитать этот замечательный обзор: М. Бьорк, 2009, Успешные методы кодирования SAT
Обе проблемы связаны с выполнимостью булевых функций. Разница заключается в способе представления функций — либо в виде схем, либо в виде формул.
В схеме выход одного вентиля может использоваться несколько раз. При переводе схемы в формулу очевидным способом решения этой проблемы является дублирование частей схемы, что может привести к экспоненциальному увеличению размера.