Jak udowodnić, że ograniczona wersja 3SAT, w której dosłowność nie może wystąpić więcej niż jeden raz, można rozwiązać w czasie wielomianowym?

Próbuję wypracować zadanie (zaczerpnięte z książki Algorytmy - S. Dasgupta, CH Papadimitriou i UV Vazirani , Rozdział 8, problem 8.6a), i parafrazuję to, co mówi:

Biorąc pod uwagę, że 3SAT pozostaje NP-kompletny, nawet jeśli ogranicza się do formuł, w których każdy literał pojawia się co najwyżej dwa razy, pokaż, że jeśli każdy literał pojawia się co najwyżej raz, to problem można rozwiązać w czasie wielomianowym.

Próbowałem rozwiązać ten problem, dzieląc klauzule na wiele grup:

1. Klauzule, które nie miały żadnej zmiennej wspólnej z resztą klauzul
2. Klauzule, które mają tylko jedną zmienną wspólną
3. Klauzule, które łączyły 2 zmienne
4. Klauzule, które łączyły wszystkie 3 zmienne

Podjęto próbę mojego rozumowania zgodnie z tym, że liczba takich grup jest skończona (z powodu nałożonego ograniczenia, że ​​dosłowność nie występuje więcej niż jeden raz), i możemy spróbować najpierw zaspokoić najbardziej ograniczoną grupę (grupa 4), a następnie zastąpić skutkują mniej ograniczonymi grupami (3, 2, a następnie 1), ale zdałem sobie sprawę, że nigdzie mnie to nie prowadzi, ponieważ nie różni się to zbytnio od przypadku ograniczonej wersji 3SAT, w której może występować każdy literał co najwyżej dwa razy, co okazało się być NP-zupełne.

Próbowałem szukać w Internecie jakichkolwiek wskazówek / rozwiązań, ale jedyne, co mogłem uzyskać, to ten link , w którym podana wskazówka nie miała dla mnie wystarczającego sensu, który odtwarzam tutaj dosłownie:

$x_i$$C_j$$x_i$$\overline{x_i}$$C_k$$C_j \lor \overline{C_k}$

$C_j$$C_k$$C_j \lor \overline{C_k}$$\overline{C_j \lor C_k}$

Jakakolwiek pomoc w odszyfrowaniu podpowiedzi lub zapewnieniu ścieżki, którą mogę zbadać, byłaby bardzo wdzięczna.

Bez utraty ogólności możemy założyć, że każda zmienna pojawia się dokładnie raz dodatnio i dokładnie raz ujemnie (jeśli zmienna pojawia się tylko raz, ustaw jej wartość, aby spełnić klauzulę i usunąć klauzulę). Możemy również założyć, że zmienna nie pojawia się w klauzuli więcej niż jeden raz (jeśli zmienna pojawia się zarówno w klauzuli pozytywnej, jak i negatywnej, wówczas klauzula jest spełniona i może zostać usunięta). Nie wpłyną one na satysfakcję.

Teraz użyj reguły rozdzielczości, aby wyeliminować zmienne jeden po drugim (ponieważ każda zmienna pojawia się dokładnie raz pozytywnie, a raz negatywnie, jest to proces deterministyczny). Jeśli w dowolnym momencie otrzymamy pustą klauzulę, zestaw klauzul jest niezadowalający, w przeciwnym razie jest zadowalający. To dlatego, że:

• rozdzielczość jest kompletnym systemem dowodu zdania (tzn. jeśli klauzula jest logicznie implikowana przez zestaw klauzul, to można ją wyprowadzić z zestawu klauzul przy użyciu tylko reguły rozdzielczości),

• zestaw klauzul jest niezadowalający, jeśli logicznie implikuje to pustą klauzulę.

$(x \lor B) \land (\overline{x} \lor C) \land \dots)$$(B \lor C) \land \dots$, która zawiera jedną klauzulę mniejszą niż przed rozstrzygnięciem. Przeciwnie, jeśli zastosujesz to do formuły 3SAT bez ograniczenia liczby wystąpień każdego literału, zastosowanie rozdzielczości może spowodować wykładniczy wzrost liczby klauzul.