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.