@Mirek SAT je testování splnitelnosti výrokových formulí. Používá se například v umělé inteligenci, návrhu integrovaných obvodů nebo testování korektnosti softwaru. Jde o NP-úplný problém, pro nějž ale existují superrychlé algoritmy. Typicky se nějaký komplexní problém převede na SAT, vyřeší a pak se z valuace dekóduje řešení. Hezký příklad praktického využití je třeba SATPLAN (viz wiki, google).
