Klauzula oparta na konflikcie Wyjaśnienie uczenia się nawrotu

Na stronie wikipedia tutaj całkiem dobrze opisuje algorytm CDCL (i wydaje się, że zdjęcia zostały zrobione ze slajdów stworzonych przez Sharada Malika z Princeton). Jednak przy opisywaniu sposobu cofania wszystko mówi „do właściwego punktu”. MiniSAT wykorzystuje również wariant algorytmu CDCL, więc przeczytałem ten artykuł. Wydaje się, że mówią, że powinieneś cofać się, dopóki wyuczona klauzula nie będzie klauzulą ​​jednostkową. To z pewnością wyjaśnienie, ale nie ma dla mnie sensu. Ostatnie zadanie z pewnością będzie częścią wyuczonej klauzuli konfliktu, o ile mogę powiedzieć (być może tutaj się mylę?), Więc gdy cofniesz się o jeden krok, natychmiast utworzysz wyuczoną jednostkę klauzuli, ostatnia przypisana wartość zostanie odwrócona, a algorytm będzie działał dokładnie tak, jak DPLL, bez cofania się wystarczająco daleko. Dodatkowo strona wikipedia nie przestrzega tej zasady, cofa się o wiele dalej, co wydaje się pożądane.

Jak daleko należy się wycofać?

Oto odpowiedni akapit z artykułu MiniSAT:

Faza decyzyjna będzie trwała do momentu przypisania wszystkich zmiennych, w którym to przypadku mamy model lub doszło do konfliktu. W przypadku konfliktów wywoływana jest procedura uczenia się i tworzona jest klauzula konfliktu. Ścieżka będzie używana do cofania decyzji, jeden poziom na raz, dopóki dokładnie jeden z literałów wyuczonej klauzuli nie zostanie powiązany (wszystkie są$False$w punkcie konfliktu). Z założenia klauzula konfliktu nie może przejść bezpośrednio z konfliktu do klauzuli z dwoma lub więcej literami niezwiązanymi. Jeśli klauzula pozostaje jednostką dla kilku poziomów decyzyjnych, korzystne jest wybranie [sic] najniższego poziomu (określanego jako skok wsteczny lub niechronologiczny powrót ).

Chyba nie zauważyłeś, że gdy wyuczona klauzula stanie się jednostką z powodu cofniętych przypisań (cofanie), solver nie kończy się na tym. Mogą istnieć inne zadania przed tym, które nie mają wpływu na bieżący konflikt i eksperymentalnie wykazano, że lepiej jest również cofnąć te niepowiązane zadania. Zatem solver kontynuuje cofanie przypisań, dopóki następne cofnięcie nie uczyniłoby wyuczonej klauzuli jednostką, tj. Zawierałoby więcej niż jedną nieprzypisaną zmienną. Solver zatrzymuje się tutaj, uruchamia propagację jednostek, aby spełnić klauzulę unit, a następnie wznawia wyszukiwanie, normalnie przypisując zmienne.

Należy również zauważyć, że bieżąca zmienna decyzyjna może nie być obecna w wyuczonej klauzuli. Powszechną strategią dla solwera CDCL jest znalezienie pierwszego unikalnego punktu implikacji i użycie tej zmiennej w wyuczonej klauzuli. W niektórych przypadkach pierwszy UIP jest zmienną decyzyjną, ale często nie jest.