Presná definícia
Čo znamená problém splniteľnosti?
Problém splniteľnosti sa pýta, či existuje interpretácia alebo priradenie, v ktorom sú všetky formule či obmedzenia súčasne pravdivé. Výroková verzia SAT je kanonický NP-úplný problém; iné logiky majú odlišnú zložitosť alebo rozhodnuteľnosť. Odpoveď SAT často zahŕňa model, UNSAT môže mať dôkaz.
Skúsenosť a kontext
Ako sa pojem používa v praxi
Konfigurátor prevedie požiadavky na CNF a pred publikovaním overí, že aspoň jedna konfigurácia existuje. Pri UNSAT solver vráti jadro konfliktujúcich klauzúl, ktoré sa preloží späť na obchodné pravidlá. Testy porovnajú preklad s ručne známymi prípadmi.
Overiteľnosť
Odborné zdroje
Praktické odpovede
Často kladené otázky
Ako funguje problém splniteľnosti?
Solver hľadá pravdivostné priradenie spĺňajúce všetky klauzuly alebo systematicky dokáže, že žiadne neexistuje.
Kedy má problém splniteľnosti praktický význam?
Konfigurátor prevedie požiadavky na CNF a pred publikovaním overí, že aspoň jedna konfigurácia existuje.
S čím si pojem nezamieňať?
Platnosť sa pýta, či formula platí vo všetkých interpretáciách; satisfiabilita, či platí aspoň v jednej.
Ako sa výsledok kontroluje?
Overuje sa model dosadením, UNSAT certifikátom, malými brute-force prípadmi a mapovaním klauzúl na požiadavky.
Na čo si dať pozor?
Najťažšia chyba býva v kódovaní domény, nie v solveri; veľké inštancie môžu mať nepredvídateľný čas.