Problemet med tilfredsstillelse af boolske formler ( SAT , vyp ) er et algoritmisk problem vigtigt for teorien om beregningsmæssig kompleksitet .
En opgaveinstans er en boolsk formel , der kun består af variabelnavne, parenteser og operationer ( AND ), ( OR ) og ( HE ). Problemet er: er det muligt at tildele falske og sande værdier til alle variabler, der forekommer i formlen , så formlen bliver sand.
Ifølge Cooks teorem , bevist af Stephen Cook i 1971, er SAT-problemet for boolske formler skrevet i konjunktiv normalform NP-komplet . Kravet om at skrive i konjunktiv form er væsentligt, da for eksempel SAT-problemet for formler præsenteret i disjunktiv normalform løses trivielt i lineær tid afhængigt af størrelsen af formelposten (for at formlen skal være tilfredsstillende, kun tilstedeværelsen af mindst én konjunktion er påkrævet , der ikke samtidig indeholder og negation for en variabel ).
For at formulere genkendelsesproblemet præcist er der fastsat et endeligt alfabet, ved hjælp af hvilket sprogforekomster specificeres. Hopcroft , Motwani og Ullman foreslår i deres bog Introduction to Automata Theory , Languages and Computation at bruge følgende alfabet :.
Når du bruger dette alfabet, skrives parenteser og operatorer naturligt, og variabler får følgende navne: , ifølge deres tal i binær notation .
Lad en boolsk formel , skrevet i den sædvanlige matematiske notation, have længden af tegn. I den blev hver forekomst af hver variabel beskrevet af mindst et symbol, derfor er der ikke mere end variabler i denne formel. Det betyder, at i den ovenfor foreslåede notation vil hver variabel blive skrevet ved hjælp af symboler. I dette tilfælde vil hele formlen i den nye notation have længden af tegn, det vil sige, at længden af strengen vil stige med et polynomium antal gange.
For eksempel vil formlen have formen .
I et papir fra 1970 af Stephen Cook blev udtrykket " NP-komplet problem " først introduceret , og SAT-problemet var det første problem, som denne egenskab blev bevist for.
I beviset for Cooks teorem er hvert problem fra klassen NP eksplicit reduceret til SAT. Efter fremkomsten af Cooks resultater blev NP-fuldstændighed bevist for mange andre problemer. I dette tilfælde, som oftest, for at bevise NP-fuldstændigheden af et bestemt problem, gives polynomiumreduktionen af SAT-problemet til det givne problem, muligvis i flere trin, det vil sige ved hjælp af flere mellemliggende problemer.
Interessante vigtige specialtilfælde af SAT-problemet er:
En af de mest effektive metoder til at parallelisere SAT-opgaver er CDCL-løsere (CDCL, engelsk konfliktdrevet klausulindlæring ), baseret på ikke-kronologiske varianter af DPLL-algoritmen [1] [2] .
NP-komplette problemer | |
---|---|
Maksimeringsproblem ved stabling (pakning) |
|
grafteori mængdeteori | |
Algoritmiske problemer | |
Logiske spil og puslespil | |