== include(page="template/taskheader" task_id="2sat") ==

Problema satisfiabilităţii, notată prescurtat cu 'SAT':http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Basic_definitions.2C_terminology_and_applications, cere determinarea existenţei unei atribuiri satisfiabile pentru o formulă booleană. O atribuire de valori booleene pentru variabilele acestei expresii se numeşte „atribuire satisfiabilă” dacă evaluarea expresiei după atribuirea valorilor are ca rezultat valoarea de adevăr „adevărat”. Următoarea formulă: <tex> ((x_{1} \rightarrow x_{2}) \vee \sim((\sim x_{1} \leftrightarrow x_{3}) \vee x_{4})) \wedge \sim x_{2} </tex>, are o atribuire satisfiabilă dată de: <tex> \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle </tex>.

Problema satisfiabilităţii, notată prescurtat cu 'SAT':http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Basic_definitions.2C_terminology_and_applications, cere determinarea existenţei unei atribuiri satisfiabile pentru o formulă booleană. O atribuire de valori booleene pentru variabilele acestei expresii se numeşte „atribuire satisfiabilă” dacă evaluarea expresiei după atribuirea valorilor are ca rezultat valoarea de adevăr „adevărat”. Următoarea formulă: <tex> ((x_{1} \rightarrow x_{2}) \vee ((\bar{x_{1}} \leftrightarrow x_{3}) \wedge x_{4})) \wedge \bar{x_{2}} </tex>, are o atribuire satisfiabilă dată de: <tex> \langle x_{1} = 0, x_{2} = 0, x_{3} = 1, x_{4} = 1 \rangle </tex>.

Utilizând următoarele 'echivalenţe logice':http://en.wikipedia.org/wiki/Logical_equivalence: 'regula dublei negaţii':http://en.wikipedia.org/wiki/Double_negative_elimination, 'legile lui De Morgan':http://en.wikipedia.org/wiki/De_Morgan%27s_laws şi 'legea distributivităţii':http://en.wikipedia.org/wiki/Distributivity, orice formulă booleană poate fi transformată în 'forma normal conjunctivă':http://en.wikipedia.org/wiki/Conjunctive_normal_form, o expresie scrisă ca o conjuncţie de propoziţii, iar fiecare propoziţie ca o disjuncţie de literali. Un exemplu de expresie în forma normal conjunctivă este: <tex> (x_{1} \vee x_{3}) \wedge (x_{2} \vee \bar{x_{1}}) \wedge (\bar{x_{4}} \vee x{3}) </tex>.