Chtel bych se pochlubit se svym resenim (ktere mi proslo).
Priklad 1
Nakreslil jsem Medveduv bitonicky sort a popsal vse kolem nej.
Priklad 2
Protoze cisla z musi byt koreny, muzeme pouzit konstrukci polynomu P(x)=(x-z_0)(x-z_1)...*(x-z_{n-1}). Obycejne roznasobovani ale trva prilis dlouho - muzeme ho zrychlit pomoci Fouriera. Kdyz se alg. naimplementuje takto, bude mit pozadovanou slozitost.
Priklad 3
Pro jistotu uvadim cely algoritmus vc. odvozeni, protoze Cepek rikal, ze je spravne, ale ze je hodne zvlastni, a chvili mu trvalo, nez ho pochopil.
Vstup: splnitelna formule F v CNF s promennymi a_1..a_n, cerna skrinka
Vystup: libovolne ohodnoceni f formule F, ve kterem je splnena
Zacneme s nulovym ohodnocenim f a prazdnou mnozinou K.
Opakujeme:
Pokud |K|=n, skoncime (byly ohodnoceny vsechny promenne).
Sestrojime formuli X=F and A, kde A je disjunkci vsech promennych a_i, ktere nejsou v K.
X je v CNF, pustime na ni cernou skrinku a zjistime, jestli je splnitelna.
Pokud X neni splnitelna, skoncime. Formule F je splnitelna a X nikoli. Vsechna splnujici ohodnoceni F tedy musi vyzadovat, aby promenne v A byly ohodnoceny nulou (coz jsou implicitne).
Pokud X je splnitelna zkonstruujeme pro kazde a_i mimo K formuli F_i=F and a_i.
Formule F_i jsou v CNF. Prozeneme je cernou skrinkou a zjistime, ktere z nich jsou splnitelne.
Protoze X je splnitelna, musi alespon jedna F_i byt take splnitelna, oznacme ji F_q.
Nastavime ohodnoceni f(a_q)=1, pridame a_q do K a nastavime F=F_q.
Slozitost: V kazdem kroku cyklu ohodnotime alespon jednu promennou, probehne tedy O(n) kroku cyklu. Uvnitr kazdeho kroku cyklu otestujeme O(n) formuli. Pokud je slozitost cerne skrinky B. Je slozitost kroku cyklu O(nB). Celkova slozitost algoritmu tedy je O(n^2B), coz je pro polynomialni B (predpoklad) polynomialni velicina.
Invariant: Na konci kazdeho kroku cyklu je formule F splnitelna a promenne z mnoziny K jsou spravne ohodnocene.
Dukaz (indukci). Na pocatku je F zadana jako splnitelna a mnozina K prazdna - invariant plati trivialne. V prubehu algoritmu jako F nastavujeme F_q, coz je opet splnitelna formule (viz jeji definice). Do mnoziny K pridavame promennou a_q. Protoze F_q je splnitelna, musi existovat ohodnoceni F, ve kterem je a_q ohodnocena jednickou. Tato promenna je tedy spravne ohodnocena.
Spravnost: Necht buno nalezene ohodnoceni f ohodnoti promenne a_1..a_k jednickou a promenne a_{k+1}..a_n nulou (jinak je precislujeme). Kdyz algoritmus skonci, formule F je ve tvaru (A and a_1 and a_2 and ... and a_k). Algoritmus se mohl zastavit ve dvou mistech.
Pokud se zastavil kvuli |K|=n, pak jsou vsechny promenne spravne ohodnocene (viz invariant).
Pokud se zastavil, protoze je X nesplnitelna, podivame se na X, ktera vypada takto: (F and (a_{k+1} or a_{k+2} or ... or a_n)). Protoze je F splnitelna a X ne, musi byt problem v poslednim clenu. Ten muze splnitelnost X pokazit jen pokud vsechna splnujici ohodnoceni F priradi promennym a_{k+1}..a_n nulu. To je ale implicitni hodnota ohodnoceni pro tyto promenne, takze jsou spravne ohodnoceny. Zbyle promenne jsou v K a diky invariantu vime, ze jsou take spravne ohodnoceny.
Matfyz Wiki