Jak stwierdzono w Podwójne heurystyki widzenia dla Problemów satysfakcji Binary Ograniczenie (PA Geelen):
kanalizowania ograniczeń dwóch różnych modeli pozwala na wyrażanie relacji między dwoma zbiorami zmiennych, po jednym każdego Model.
Oznacza to zadania w jednym z punktów widzenia, może być tłumaczony na zadania w drugiej i vice versa, jak również, gdy inicjuje wyszukiwanie, wartości wykluczone z jednego modelu można wykluczyć od siebie, jak również.
Pozwól mi rzucić przykład, który zaimplementowałem jakiś czas temu, pisząc narzędzie do rozwiązywania sudoku.
klasyczny punkt widzenia
Tu zinterpretować ten problem w taki sam sposób człowiek będzie: za pomocą liczby całkowite od 1 do 9 i definicji, że wszystkie wiersze, kolumny i bloki musi zawierać każdą liczbę całkowitą dokładnie raz.
Możemy łatwo stwierdzić to w Eclipse przy użyciu coś jak:
% Domain
dim(Sudoku,[N,N]),
Sudoku[1..N,1..N] :: 1..N
% For X = rows, cols, blocks
alldifferent(X)
I to jest jeszcze wystarczające, aby rozwiązać zagadkę Sudoku.
Binary logiczna widzenia
Można by jednak wybrać do reprezentowania liczb całkowitych przez ich binarnych tablic logicznych (pokazanych w answer przez @jschimpf). W przypadku, gdy nie jest jasne, co to jest, za mały przykład poniżej (jest to wbudowany w funkcjonalności!):
? ic_global:bool_channeling(Digit, [0,0,0,1,0], 1).
Digit = 4
Yes (0.00s cpu)
? ic_global:bool_channeling(Digit, [A,B,C,D], 1), C = 1.
Digit = 3
A = 0
B = 0
C = 1
D = 0
Yes (0.00s cpu)
Jeśli użyjemy tego modelu do reprezentowania Sudoku, każdy numer zostanie zastąpiony przez jego binarnej wartości logicznej tablica i odpowiednie ograniczenia mogą być zapisane.Będąc trywialnym dla tej odpowiedzi, nie będę zawierał całego kodu dla ograniczeń, ale ograniczenie pojedynczej sumy wystarczy, aby rozwiązać zagadkę sudoku w jej binarnej reprezentacji boolowskiej.
Channeling
Mając te dwa punkty widzenia z odpowiednimi ograniczonych modeli daje teraz możliwość kanał między nimi i sprawdzić, czy wszelkie ulepszenia zostały wykonane.
Ponieważ oba modele są nadal tylko płytą NxN, nie ma różnicy w wymiarze reprezentacji, a channeling staje się naprawdę łatwy.
Pozwól mi najpierw dać ostatni przykład co blok wypełniony liczbami całkowitymi 1..9 będzie wyglądać w obu naszych modeli:
% Classic viewpoint
1 2 3
4 5 6
7 8 9
% Binary Boolean Viewpoint
[](1,0,0,0,0,0,0,0,0) [](0,1,0,0,0,0,0,0,0) [](0,0,1,0,0,0,0,0,0)
[](0,0,0,1,0,0,0,0,0) [](0,0,0,0,1,0,0,0,0) [](0,0,0,0,0,1,0,0,0)
[](0,0,0,0,0,0,1,0,0) [](0,0,0,0,0,0,0,1,0) [](0,0,0,0,0,0,0,0,1)
Teraz wyraźnie widać związek między modelami i po prostu napisz kod, aby skierować nasze zmienne decyzyjne. Korzystanie Sudoku i BinBools jako naszych płyt, kod będzie wyglądał mniej więcej tak:
(multifor([Row,Col],1,N), param(Sudoku,BinBools,N)
do
Value is Sudoku[Row,Col],
ValueBools is BinBools[Row,Col,1..N],
ic_global:bool_channeling(Value,ValueBools,1)
).
W tym momencie mamy przekazywany model, w którym, w trakcie poszukiwań, jeśli wartości są oczyszczone w jednym z modeli, jego wpływ nastąpi również w drugim modelu. To może oczywiście prowadzić do dalszej ogólnej propagacji ograniczeń.
Rozumowanie
Aby wyjaśnić przydatność binarnym modelu logicznego dla Sudoku, musimy najpierw rozróżnić niektórych przewidzianych alldifferent/1 wdrożeń przez Eclipse:
Co to oznacza w praktyka może być pokazana w następujący sposób:
? [A, B, C] :: [0..1], ic:alldifferent([A, B, C]).
A = A{[0, 1]}
B = B{[0, 1]}
C = C{[0, 1]}
There are 3 delayed goals.
Yes (0.00s cpu)
? [A, B, C] :: [0..1], ic_global:alldifferent([A, B, C]).
No (0.00s cpu)
Ponieważ nie było jeszcze żadnych przydziałów przy użyciu sprawdzania przekazywania (biblioteka ic), nieważność kwerendy nie została jeszcze wykryta, natomiast wersja zgodna Bound natychmiast to zauważa. Takie zachowanie może prowadzić do znacznych różnic w propagacji ograniczeń podczas przeszukiwania i przechodzenia przez mocno ograniczone modele.
Na górze tych dwóch bibliotek znajduje się biblioteka ic_global_gac przeznaczona do globalnych ograniczeń, dla których zachowana jest uogólniona spójność łuku (nazywana również konsystencją hiper łuku lub spójnością domeny). To wyjątkowe ograniczenie/1 zapewnia jeszcze więcej możliwości przycinania niż spójne, jednoznaczne, , ale zachowanie pełnej spójności domeny ma swój koszt, a korzystanie z tej biblioteki w mocno ograniczonych modelach generalnie prowadzi do utraty wydajności działania.
Z tego powodu odkryłem, że interesująca dla Sudoku jest próba pracy z spójną (ic_global) implementacją alldifferent w celu zmaksymalizowania wydajności, a następnie samodzielne podejście do spójności domeny przez channeling binarnego modelu boolowskiego.
Experiment results
Poniżej znajdują się wyniki BackTrack dla Sudoku 'platinumblonde' (wskazanej jako najtrudniejszy, najbardziej chaotyczny Sudoku łamigłówka do rozwiązania w The Chaos Within Sudoku, M. i Z. Toroczkai ErcseyRavasz), stosując odpowiednio naprzód sprawdzenie, spójność granic, spójność domeny, autonomiczną binarnego modelu logiczną i wreszcie, kierowane model:
(ic) (ic_global) (ic_global_gac) (bin_bools) (channelled)
BT 6 582 43 29 143 30
Jak widać, nasza kierowana modelu (przy użyciu Granice obszaru spójności (ic_global)) musi jeszcze jeden backtrack więcej niż spójna implementacja domeny, ale zdecydowanie działa lepiej niż samodzielna wersja spójna.
Kiedy przyjrzymy się teraz czasowi działania (wyniki są wynikiem obliczenia średniej z wielu wykonań, aby uniknąć ekstremów), z wyjątkiem sprawdzania sprawdzania postępu, ponieważ udowodniono, że nie jest już interesujący w rozwiązywaniu zagadek sudoku:
(ic_global) (ic_global_gac) (bin_bools) (channelled)
Time(ms) 180ms 510ms 100ms 220ms
Patrząc na te wyniki, myślę, że możemy z powodzeniem zakończyć eksperyment (wyniki te zostały potwierdzone przez ponad 20 innych przypadkach Sudoku):
Channeling binarne logiczną punkt widzenia na granicach zgodne autonomicznych Implementacja zapewnia nieco mniej silne propagowanie ograniczeń niż w przypadku samodzielnej implementacji w domenie, ale z czasem działania od równie długiego do znacznie szybszego.
EDIT: Próba wyjaśnienia
Wyobraźmy sobie pewną domenę zmienną reprezentującą komórkę na pokładzie Sudoku posiada pozostały domenę 4..9. Wykorzystując spójność granic, gwarantuje się, że zarówno dla wartości 4, jak i 9 można znaleźć inne wartości domeny, które spełniają wszystkie ograniczenia, a tym samym zapewniają spójność. Jednak nie ma wyraźnej gwarancji na inne wartości w domenie (taka jest "spójność domeny").
Korzystanie binarny logiczną modelu, definiujemy dwa następujące ograniczenia Suma:
- Suma wszystkich binarnym logicznej tablicy jest zawsze równa 1
- Suma każdego elementu N'th każdej tablicy w każdym wierszu/col/block jest zawsze równy 1
Dodatkowa siła wiązania jest egzekwowana przez drugie ograniczenie, które oprócz ograniczania wiersza, kolumn i bloków również domyślnie mówi: "każda komórka może zawierać tylko co cyfra jeden raz ". To zachowanie nie jest aktywnie wyrażane, gdy stosuje się tylko granice spójne alldifferent/1 constraint!
Wnioski
Oczywiste jest, że skierowanie może być bardzo przydatne do poprawy autonomicznego ograniczony model, jednak czy nowy model jest ograniczenie się wytrzymałości jest słabszy niż w obecnym modelu, oczywiście, żadnych ulepszeń będzie być zrobione. Zauważ też, że posiadanie bardziej ograniczonego modelu nie musi koniecznie oznaczać ogólnej lepszej wydajności!Dodanie większej liczby ograniczeń zmniejszy ilość backtracków potrzebnych do rozwiązania problemu, ale może również wydłużyć czas działania programu, jeśli konieczne będzie więcej sprawdzeń ograniczeń.
Ładne pytanie! Podręcznik zawiera ponad 900 stron, nie mogę znaleźć akapitu, który cytujesz. Czy możesz podać podpowiedź? – CapelliC
@CapelliC Cholera, lepiej późno niż wcale, strona 392 na dole. – Stanko