Spełnialność formuł logicznych

Ogólnie rzecz biorąc problem spełnialności formuł logicznych jest bardzo złożony pod względem obliczeniowym. Przy tym naiwny algorytm który rozwiązuje ten problem jest bardzo prosty. W Prologu można go zapisać tak:

:- op(900,fy,neg).
:- op(1000,yfx,and).
:- op(1010,yfx,or).

sat( X ) :- eval( X, true ),!.

eval( true, true ) :- !.
eval( false, false ).

eval( neg X, true ) :- eval( X, false ).
eval( neg X, false ) :- eval( X, true ), !.
eval( X or Y, true ) :- ( eval( X, true ) ; eval( Y, true ) ), !.
eval( X and Y, true ) :- eval( X, true ), eval( Y, true ), !.

eval( X, false ) :- eval( X, true ), !, fail.
eval( _, false ).

Korzystamy tutaj mocno z wbudowanego w Prolog backtrackingu. Możemy sprawdzać spełnialność formuł w stylu

X or Y and neg (Y and X)

Przykładowa sesja:

?- [sat].
% sat compiled 0.00 sec, 2,936 bytes

Yes
?- sat( neg neg neg X ).

X = false ;;

No
?- sat( neg neg neg X and neg Y).

X = false,
Y = false ;;

No
?- sat( neg neg neg X and neg Y and Z).

X = false,
Y = false,
Z = true ;;

No
?- sat( X and neg X ).

No
?- sat( _ and neg _ ).

Yes
?-
% halt

Jak widać Prolog bywa zręcznym narzędziem do wyrażania pewnych algorytmów.

Minus jeden, czyli co aktualnie porabiam

Studiuję aktualnie w -1, zwanym też ii, II, albo Instytutem Informatyki Uniwersytetu Wrocławskiego. Fajnie nie?

Ano fajnie, bo wydział należy do tych wybitnie fajnych. Ficzery:
- za wyjątkiem 8 obowiązkowych przedmiotów (po 2 przez pierwsze 4 semestry) program studiów jest układany samodzielnie przez studenta. Chcę się zapisać na przedmiot XYZ? Robię to. Chcę się z niego wypisać? Przez pierwsze dwa tygodnie semestru można to robić bez konsekwencji.
- wysoki poziom. Serio, nie żartuję - jest się tu czego nauczyć i daje to ogromną satysfakcję. Później także dobry start na rynku pracy, ale to już szczegół :-) Kilku absolwentów pracuje nawet dla Google czy M$, inni założyli jakiś portal społecznościowy
- atmosfera, nie tylko dzięki klimatyzacji w budynku. Wśród studentów panuje spora różnorodność osobowości i zawsze znajdzie się ktoś, z kim można porozmawiać.
- mniej ważne, ale jednak: fajny, nowy budynek położony dogodnie przy Moście Grunwaldzkim.

Szczęśliwie zaliczyłem pierwszy rok i jestem aktualnie na 4-tym semestrze. Nie mam nawet tak u nas popularnej poprawki z Programowania :-) Choć być może uda mi się coś wymyślić z JFiZo (Języki Formalne i ZŁOżoność Obliczeniowa), którego rokrocznie zdaje jakieś 30% osób. To raczej mało, szczególnie że wiele z tych, którym się udaje, robi ten przedmiot nie po raz pierwszy. AiSD (Algorytmy i Struktury Danych) też są obiecujące w tym względzie.

Przedmioty na których najlepiej się bawiłem? Będzie jakoś tak:
1. Programowanie (Haskell rządzi!)
2. Programowanie funkcjonalne (niefajny był tam OCaml, ale poznałem podstawy tego paradygmatu)
3. Przetważanie Języka Naturalnego (Natural Language Processing, NLP) (program do pisanie wierszy)
4. Kurs C (grupa zaawansowana: graficzna gra w Sudoku, gra 3D, kalkulator+wykresy 3D, znajdowanie trasy przejazdu komunikacją miejską we Wrocławiu)

Na razie to tyle, stay tuned.