Problem zadovoljivosti naziva se i Boolean satisfiability problem, propositional satisfiability problem, i uobičajeno se piše skraćeno SAT ili B-SAT. Suština problema je određivanje da li postoji interpretacija koja zadovoljava datu logičku formulu.
Interpretacija je jedan oblik logičke formule, odnosno skup vrednosti parametara, takav da formula može da se izračuna i da logičku vrednost. Interpretacija formule f = (-p * -s) + (p * r) bila bi npr: za p=1, r=1, s=1 formula ima vrednost 1. Ova interpretacija proizvodi tačnu vrednost logičke formule, i predstavlja slučaj koji zadovoljava tu formulu, odnosno pokazuje da formula može da ima tačnu vrednost ako se parametri postave kako treba.
Algoritmi koji rešavaju problem zadovoljivosti rade tako što određuju da li formula ima takvu intepretaciju.
Interpretacija
Za formulu u kojoj se pojavljuje samo jedan parametar, npr. F = p + -p, postoji dve moguće interpretacije: p=1 i p=0.
Za formulu u kojoj se pojavljuje dva parametra, p i q, postoji 4 moguće interpetacije (dva parametra, svaki po dve moguće logičke vrednosti).
Za formulu u kojoj se pojavljuje tri parametra, p,q,r, postoji 8 mogućih interpretacija.
Možemo da zaključimo (a ranije smo primetili, posebno kod karnoovih mapa) da je broj mogućih interpretacija jednak dvojci stepenovanoj na broj parametara: za tri parametra imamo 23=8 mogućih interpretacija.
Ako nijedna nije tačna to je nezadovoljiva formula.
Ako je bar jedna interpretacija tačna to je zadovoljiva formula.
Ako su sve interpretacije tačne to je tautologija, koja je usput i zadovoljiva formula.
Zadovoljivost možemo da drugim rečima opišemo i kao: postoji takav slučaj (takve vrednosti parametara) u kome je formula tačna.
Nezadovoljivost možemo da dokažemo tako što uzmemo negaciju izraza i dokažemo da je negacija tautologija (uvek tačna).
Zadovoljivost možemo da dokažemo tako što utvrdimo da postoji takav slučaj koji zadovoljava formulu.
Zadovoljivost možemo da dokažemo tako što dokažemo da formula nije nezadovoljiva – odnosno, tako što uzmemo negaciju formule, dokažemo da nije tautologija, i time pokažemo da postoje slučajevi u kojima negacija formule nije tačna, tj. formula jeste tačna.
Ovo je interesantno zato što konstrukcija algoritma koji dokazuje tautologiju može biti zgodnija od algoritma koji traži postojanje slučaja zadovoljenja.