Spojrzenie w przyszłość (cofanie się)

W algorytmach śledzenia wstecznego patrzenie w przyszłość jest ogólnym terminem określającym podprocedurę , która próbuje przewidzieć skutki wyboru zmiennej rozgałęziającej w celu oceny jednej z jej wartości. Dwa główne cele przewidywania w przód to wybór zmiennej do oceny w następnej kolejności oraz kolejność wartości, które mają zostać jej przypisane.

Zadowolenie z ograniczeń

W ogólnym problemie spełniania ograniczeń każda zmienna może przyjąć wartość w dziedzinie. Dlatego algorytm śledzenia wstecznego iteracyjnie wybiera zmienną i testuje każdą z jej możliwych wartości; dla każdej wartości algorytm jest rekurencyjnie . Spojrzenie w przyszłość służy do sprawdzania skutków wyboru danej zmiennej do oceny lub do decydowania o kolejności nadania jej wartości.

Techniki patrz w przyszłość

W tym przykładzie brane jest pod uwagę x ₁ = 2 i wstępne przypisanie x ₂ = 1.

Sprawdzanie w przód sprawdza tylko, czy każda z nieprzypisanych zmiennych x ₃ i x ₄ jest zgodna z częściowym przypisaniem, usuwając wartość 2 z ich domen.

Prostszą techniką oceny efektu określonego przypisania do zmiennej jest sprawdzanie w przód . Biorąc pod uwagę bieżące rozwiązanie częściowe i przypisanie kandydata do oceny, sprawdza, czy inna zmienna może przyjąć spójną wartość. Innymi słowy, najpierw rozszerza bieżące rozwiązanie częściowe o wstępną wartość rozważanej zmiennej; następnie bierze pod uwagę każdą inną zmienną $,$ czy istnieje ocena $k}}$ co jest zgodne z rozszerzonym rozwiązaniem częściowym. $Mówiąc bardziej ogólnie, sprawdzanie w$ określa wartości dla które są zgodne z rozszerzonym przypisaniem.

Spójność łuku z wyprzedzeniem sprawdza również, czy wartości x ₃ i x ₄ są ze sobą spójne (czerwone linie), usuwając również wartość 1 z ich dziedzin.

Technika wyprzedzająca, która może być bardziej czasochłonna, ale może dawać lepsze wyniki, opiera się na spójności łuku . Mianowicie, biorąc pod uwagę częściowe rozwiązanie rozszerzone o wartość dla nowej zmiennej, wymusza spójność łuku dla wszystkich nieprzypisanych zmiennych. Innymi słowy, w przypadku dowolnych nieprzypisanych zmiennych usuwane są wartości, których nie można konsekwentnie rozszerzyć na inną zmienną. Różnica między sprawdzaniem w przód a spójnością łuku polega na tym, że ta pierwsza sprawdza spójność tylko jednej nieprzypisanej zmiennej w czasie, podczas gdy druga sprawdza również pary nieprzypisanych zmiennych pod kątem wzajemnej spójności. Najpowszechniejszym sposobem wykorzystania przewidywania do rozwiązywania problemów spełniania ograniczeń jest tzw utrzymywanie algorytmu spójności łuku (MAC) .

Dwie inne metody obejmujące spójność łuku to pełne i częściowe spojrzenie w przyszłość. Wymuszają spójność łuku, ale nie dla każdej pary zmiennych. $wygląd$ uwzględnia każdą parę nieprzypisanych zmiennych i wymusza spójność Różni się to od wymuszania globalnej spójności łuku, co może wymagać ponownego rozważenia pary zmiennych więcej niż jeden raz. Zamiast tego, gdy pełne spojrzenie w przyszłość wymusi spójność łuku między parą zmiennych, para nie jest już brana pod uwagę. Częściowe spojrzenie w przyszłość jest podobne, ale brana jest pod uwagę określona kolejność zmiennych, a spójność łuku jest wymuszana tylko raz dla każdej pary ${\ displaystyle x_ {i}, x_ {j}}$ z ja $\ displaystyle i <j}$ .

Spojrzenie w przyszłość w oparciu o spójność łuku można również rozszerzyć, aby pracować ze spójnością ścieżki i ogólną spójnością i lub relacyjną spójnością łuku.

Użycie patrzenia w przyszłość

Wyniki wyszukiwania w przód są wykorzystywane do decydowania o następnej zmiennej do oceny i kolejności wartości, które mają zostać nadane tej zmiennej. W szczególności dla każdej nieprzypisanej zmiennej i wartości funkcja prognozowania szacuje skutki ustawienia tej zmiennej na tę wartość.

Wybór następnej zmiennej i wybór następnej wartości do jej nadania uzupełniają się, ponieważ wartość jest zwykle wybierana w taki sposób, aby rozwiązanie (jeśli takie istnieje) zostało znalezione tak szybko, jak to możliwe, podczas gdy zwykle wybierana jest następna zmienna w taki sposób niespełnialność (jeśli obecne rozwiązanie cząstkowe jest niespełnialne) jest udowodniona tak szybko, jak to możliwe.

Wybór następnej zmiennej do oceny jest szczególnie ważny, ponieważ może powodować wykładnicze różnice w czasie wykonywania. W celu jak najszybszego udowodnienia niespełnialności preferowane są zmienne pozostawiające po przypisaniu niewiele alternatyw. Idea ta może być zrealizowana poprzez sprawdzenie jedynie spełnialności lub niespełnialności par zmienna/wartość. W szczególności następną wybraną zmienną jest ta, która ma minimalną liczbę wartości zgodnych z bieżącym rozwiązaniem częściowym. Z kolei spójność można ocenić, po prostu sprawdzając częściową spójność lub stosując dowolną z rozważanych technik wyprzedzania omówionych powyżej.

Poniżej przedstawiono trzy metody porządkowania wartości, które mają zostać wstępnie przypisane do zmiennej:

1. min-konflikty: preferowanymi wartościami są te, które usuwają najmniejszą sumę wartości z domeny nieprzypisanych zmiennych, zgodnie z oceną z wyprzedzeniem;
2. max-domain-size: preferencja zmiennej jest odwrotnością liczby wartości w najmniejszej domenie, które wytwarzają dla nieprzypisanych zmiennych, zgodnie z oceną z wyprzedzeniem;
3. estymuj rozwiązania: preferowanymi wartościami są te, które dają maksymalną liczbę rozwiązań, ocenianych przez spojrzenie w przód przy założeniu, że wszystkie wartości pozostawione w dziedzinach nieprzypisanych zmiennych są ze sobą zgodne; innymi słowy, preferencję dla wartości uzyskuje się przez pomnożenie rozmiaru wszystkich domen wynikających z patrzenia w przyszłość.

Eksperymenty dowiodły, że techniki te są przydatne w przypadku dużych problemów, zwłaszcza tych z minimalnymi konfliktami.

Randomizacja jest czasami używana do wybierania zmiennej lub wartości. Na przykład, jeśli dwie zmienne są jednakowo preferowane według jakiejś miary, wyboru można dokonać losowo.

•   Dechter, Rina (2003). Przetwarzanie ograniczeń . Morgana Kaufmanna. ISBN 1-55860-890-7
• Ouyang, Ming (1998). „Jak dobre są reguły rozgałęziania w DPLL?” . Dyskretna matematyka stosowana . 89 (1–3): 281–286. doi : 10.1016/S0166-218X(98)00045-6 .