Hlavní navigace

Názor ke článku Proč je Java za zenitem od zboj - @Mirek SAT je testování splnitelnosti výrokových formulí. Používá...

  • 20. 3. 2014 14:29

    zboj (neregistrovaný)

    @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).