A Kind of Magic – problemy spełnialności więzów (Constraint Satisfaction Problems) – część 1

Nie zawsze sposób osiągnięcia rozwiązania jest ważny, czasem liczy się tylko poprawna odpowiedź. Przykładem takiego problemu może być sudoku – trzeba wymyślić co wpisać w wolne pola, nie jest istotne w jakiej kolejności i w jaki sposób. Innym przykładem może być kolorowanie mapy – żadne dwa sąsiadujące kraje nie mogą używać tego samego koloru. Podobnie jak ustalenie planu zajęć: wykładowca i student może być tylko w jednym miejscu na raz, sala nie może mieścić dwóch wykładów jednocześnie, niektóre zajęcia wymagają określonego sprzętu etc. Tego typu problemy określa się tytułowym mianem Constraint Satisfaction Problems (CSP) lub w języku Mickiewicza: Problemy spełnialności więzów.

Jako przykładowy problem weźmy kwadraty magiczne. Chyba wszyscy spotkali się z nimi na wczesnym etapie edukacji, ale dla przypomnienia: jest to tabela (macierz) NxN z liczbami posiadająca następująca własność: suma każdego wiersza jest taka sama jak suma każdej kolumny jak również sumy obu przekątnych.

180px-Magicsquareexample.svgFormalizacja

Sformalizujmy nieco zagadnienie (przykład dla kwadratu 4×4 o sumie równej 34).
\text{Magic Square} =  \begin{pmatrix}  v_{0} & v_{1} & v_{2} & v_{3} \\  v_{4} & v_{5} & v_{6} & v_{7} \\  v_{8} & v_{9} & v_{10} & v_{11} \\  v_{12} & v_{13} & v_{14} & v_{15}  \end{pmatrix}
Mamy 16 zmiennych – po jednej na każde pole. Niektóre z nich mogą mieć już na początku ustalone wartości (mała dygresja: skoro są już ustalone to nie muszą być zmiennymi, ale takie podejście ułatwi w tym wypadku implementację).
V = (v_0, v_1, \dotsc v_{14}, v_{15})
Każda ze zmiennych przyjmuje wartości z określonej dziedziny. Ogólnie dziedzina może być dowolnym niepustym zbiorem, także ciągłym lub nieskończonym. W rozważanym przypadku jest to skończony zbiór liczb naturalnych powiedzmy od 1 do 20. (Dalsze rozważania są prowadzone dla problemów które mają skończoną dziedzinę). Każda zmienna może mieć różną dziedzinę – w szczególności gdy jej wartość jest ustalona może być to zbiór jednoelementowy.
\forall_{v \in V} \in \{1 \dotsc 20\}
Pomiędzy zmiennymi zachodzą pewne ograniczenia (więzy) mówiące o tym jak pewne zmienne mają się do siebie. Tutaj ograniczenia mówią o sumach poszczególnych wierszy/kolumn/przekątnych.
v_0 + v_1 + v_2 + v_3 = 34 \newline  v_4 + v_5 + v_6 + v_7 = 34 \newline  \vdots

Przypisaniem nazwiemy pewne przyporządkowanie (podstawienie) wartości do poszczególnych zmiennych (niekoniecznie wszystkich na raz). Przypisanie które spełnia ograniczenia będę nazywać spójnym.
Przypisanie spójne oraz kompletne (uwzględniające wszystkie zmienne) to rozwiązanie.

Jeśli ktoś pisał w Prologu to można nazwać to mniej więcej deklarowaniem ograniczeń, które wbudowany mechanizm wnioskowania będzie próbował spełnić 😉

Problem spełnialności więzów.

Tak sformułowane zagadnienie można określić jako Constraint Satisfaction Problem albo problem spełnialności więzów.

Zastanówmy się nad rozwiązaniem. Tradycyjnie zaczniemy od najprostszego a z czasem będziemy je ulepszać.

Brute force

Najprościej było by wygenerować wszystkie możliwe kombinacje. Można się jednak domyślić, że sprawdzenie tego zajmie wieki, ponadto nie ma to zbyt wiele wspólnego z jakąkolwiek inteligencją.

Backtracking search (przeszukiwanie z nawrotami)

Pomysł najlepiej będzie przedstawić na przykładzie. Załóżmy, że mamy 3 zmienne a,b,c \in \{1,2,3\} przy następujących ograniczeniach: a \ne b, b \ne c, a \ne c

csp1

Zaczynamy w korzeniu (z pustym przypisaniem). Schodzimy w dół (najpierw po lewej). Podstawienie a = 1 spełnia ograniczenia. Idziemy dalej otrzymując a = 1, b = 1. Nie spełnia ono warunków przez co cofamy się (wykonujemy nawrót). Bierzemy kolejnego potomka wierzchołka a = 1. Jest to b = 2. Podstawienie a = 1, b = 2 jest spójne. Przechodzimy w dół do węzła c = 1. Nie spełnia on warunków więc idziemy do c = 2. Tutaj podobnie: trafiamy w końcu na c = 3. Podstawienie a = 1, b = 2, c = 3 jest spójne i kompletne przez co jest rozwiązaniem.

Węzły oznaczone na czerwono to miejsca nawrotów, szare – wierzchołki nieodwiedzone.

Rekurencyjnie algorytm można zapisać w postaci:

Backtracking Search:
 1. Jeśli przypisanie jest rozwiązaniem, zakończ.
 2. v = pobierz nieprzypisaną zmienną
 3. Dla każdej wartości val z dziedziny zmiennej v:
 3.1. v = val
 3.2. Jeśli przypisanie nie spełnia ograniczeń:
 3.2.1 Oznacz v jako nieprzypisaną (lub równoważnie usuń z przypisania)
 3.2.2. Wróć do 4. (continue)
 3.3. wynik = wywołaj rekurencyjnie Backtracking Search
 3.4 Jeśli wynik jest różny od "rozwiązanie nie istnieje" zwróć wynik
 3.5 W przeciwnym wypadku ustaw v jako nieprzypisaną.
 3.6 Zwróć "rozwiązanie nie istnieje"

Implementacja

Zacznijmy od klasy reprezentującej zmienną. Przechowuje ona jej wartość lub informację, że jest nieustalona (_value = None) oraz domenę (domain). Jeśli jej wartość jest ustalona na stałe (fixed_value != None) jest to ustalane już na etapie konstrukcji obiektu. Metody __radd__, __repr__ oraz getter i setter dla value nie są istotne dla algorytmu – to szczegół implementacyjny.

class Variable(object):
    def __init__(self, fixed_value=None):
        # załpżono, że dziedzina dla wszystkich zmiennych jest taka sama [1..20]
        # ale równie dobrze może być przekazywana do konstruktora
        self.domain =  range(1,21) if fixed_value is None else [fixed_value]
        self._value = fixed_value

    # pozwala skorzystać z wbudowanej funkcji sum()
    def __radd__(self, other):
        if other is None: raise ValueError("Cannot sum None variable")
        return self.value + other

    # getter i setter dla value, rzuca wyjąktiem przy próbie przypisania
    # wartości spoza dziedziny
    @property
    def value(self):
        return self._value

    @value.setter
    def value(self, val):
        if val != None and not val in self.domain:
            raise DomainException(str(val))
        self._value = val

    def __repr__(self):
        return str(self.value)

    # informacja czy jest przypisana, tj czy value != None
    @property
    def is_assigned(self):
        return self.value != None

Klasa Assignment reprezentuje przypisanie, przechowuje listę wszystkich zmiennych. Pozwala sprawdzić kompletność oraz pobrać następną zmienną bez wartości.

class Assingment(object):
    # vars to lista zmiennych w problemie
    def __init__(self, vars):
        self.variables = vars

    # czy wszystkie zmienne mają wartość?
    def is_complete(self):
        not_assigned = [x for x in self.variables if x.value == None]
        return not not_assigned

    # weź pierwszą nieprzypisaną, jeśli takich nie ma rzuć wyjątek
    def get_unassigned_variable(self):
        for v in self.variables:
            if not v.is_assigned:
                return v
        raise AssertionError()

    # pokaż na ekranie w sensownym formacie
    def pretty_print(self):
        for i in range(0,4):
            print ' '.join(str(self.variables[i*4:i*4+4]))

Główna klasa problemu, pozwala odseparować ogólny algorytm rozwiązywania od szczegółów zagadnienia, co pozwoli łatwo korzystać z kodu dla różnych problemów. W podanej implementacji zakładamy znajomość sumy, jeżeli nie jest ona dostępna należy zmienić implementację funkcji is_violating_constraints tak aby nie przyrównywała do self.summary, ale sprawdzała czy wszystkie dają taki sam wynik.

    # sprawdza czy podstawienie narusza ograniczenia
    def is_violating_constraints(self, assigment):
        #alias coby mniej pisać 😉
        v = assigment.variables

        # spawdzenie wierszy
        for row_index in range(0,self.square_size):
            if not self.row_satisfies_constraint(row_index, v, self.summary):
                return True

        # i kolumn
        for col_index in range(0,self.square_size):
            if not self.col_satisfies_constraint(col_index, v, self.summary):
                return True

        # oraz przekątnych
        # tutaj oczywiście można zrobić to tego funkcje jak poprzednio ale już sobie odpuściłem

        if not assigment.is_complete():
            return False

        if v[0].value + v[5].value + v[10].value + v[15].value != self.summary:
            return True

        if v[3].value + v[6].value + v[9].value + v[12].value != self.summary:
            return True

        # sprawdziliśmy wszystkie warunki - dane przypisanie jest OK        
        return False

Na koniec właściwy algorytm. Warto zwrócić uwagę na fakt, że zmienna assignment jest pośrednio modyfikowana przy zmianach zmiennej var.

def backtracking_search(assignment, instance):
    # jeśli mamy rozwiązanie lub takowego nie ma - kończymy
    if assignment.is_complete() and not instance.is_violating_constraints(assignment):
        return assignment

    # pobierz zmienną bez wartości
    var = assignment.get_unassigned_variable()

    # dla wszystkich wartości z domeny zmiennej
    for val in var.domain:
        # przypisz tą wartość
        var.value = val
        # i sprawdź czy przypisanie spowodowało naruszenie więzów.
        if instance.is_violating_constraints(assignment):
            # jeśli tak cofnij przypisanie i spróbuj z następną wartością
            var.value = None
            continue
        # przypisanie było poprawne, powtórz dka kolejnej zmiennej (zejscie w dół drzewa)
        result = backtracking_search(assignment, instance)
        # mamy wynik, wróć w górę
        if result is not None:
            return result
        # niżej nie udało się spełnić ograniczeń, wyzeruj podstawienie
        else:
            var.value = None

    # nawrót
    return None

Przykładowe użycie:

magic = MagicSquare()
initial = magic.get_initial_assignment()
res = backtracking_search(initial, magic)
if res is None:
	print "Nope, nie da się."
else:
	res.pretty_print()

Sprawdźmy jak poradzi sobie z przykładowym problemem. S=34, D = \{1 \dotsc 20 \}

task

Rozwiązanie

solvedPodsumowanie

Zaprezentowany algorytm zawsze znajduje rozwiązanie (o ile oczywiście istnieje), niemniej można go znacząco ulepszyć. W następnej części sprawdzimy co jest nie tak (jak można się domyślić: wydajność) i zajmiemy się tym.

Cały kod jest dostępny na GitHubie.

Reklamy

Skomentuj

Wprowadź swoje dane lub kliknij jedną z tych ikon, aby się zalogować:

Logo WordPress.com

Komentujesz korzystając z konta WordPress.com. Wyloguj / Zmień )

Zdjęcie z Twittera

Komentujesz korzystając z konta Twitter. Wyloguj / Zmień )

Facebook photo

Komentujesz korzystając z konta Facebook. Wyloguj / Zmień )

Google+ photo

Komentujesz korzystając z konta Google+. Wyloguj / Zmień )

Connecting to %s