Elberfeld, Jakoby и Tantau 2010 ( ECCC TR10-062 ) доказали неэффективную версию теоремы Бодлендера. Они показали, что для графов с шириной дерева не более разложение дерева шириной можно найти с помощью логарифмического пространства. Постоянный множитель в границе пространства зависит от k . (Теорема Бодлендера показывает линейную временную границу с экспоненциальной зависимостью от k в постоянном множителе.)к
SAT становится легким, когда набор предложений имеет небольшую ширину. В частности, Fischer, Makowsky и Ravve 2008 показали, что выполнимость формул CNF с шириной трехугольников графа инцидентности, ограниченного можно определить с помощью не более 2 O ( k ) n арифметических операций, когда дается разложение дерева. По теореме Бодлендера, вычисление разложения дерева графа инцидентности для фиксированного k может быть выполнено за линейное время, и, следовательно, SAT может быть решено для формул с ограниченной шириной во времени, которая является полиномом низкой степени по числу переменных n .
Тогда можно было бы ожидать, что SAT должен быть на самом деле разрешимым, используя логарифмическое пространство, для формул с ограниченной шириной дерева графа инцидентности. Не ясно, как модифицировать Fischer et al. подход для принятия решения SAT в нечто экономичное пространство. Алгоритм работает путем вычисления выражения для числа решений с помощью включения-исключения и рекурсивной оценки числа решений меньших формул. Хотя ограниченная древовидная ширина действительно помогает, подформулы кажутся слишком большими для вычисления в логарифмическом пространстве.
Это заставляет меня спросить:
Известно ли, что SAT для формул с ограниченной шириной находится в или N L ?
источник
Ответы:
Действительно, используя результаты Elberfeld-Jakoby-Tantau-2010, можно показать, что SAT может быть определено в логарифмическом пространстве по формулам, у которых график инцидентности имеет ограниченную ширину дерева. Вот эскиз того, как идут основные шаги доказательства этого утверждения.
источник