Revizia anterioară Revizia următoare
Fişierul intrare/ieşire: | 2sat.in, 2sat.out | Sursă | Arhiva Educationala |
Autor | Arhiva Educationala | Adăugată de | |
Timp execuţie pe test | 0.425 sec | Limită de memorie | 65536 kbytes |
Scorul tău | N/A | Dificultate | N/A |
Vezi solutiile trimise | Statistici
2SAT
Problema satisfiabilitatii, notata prescurtat cu SAT cere determinarea existentei unei atribuiri satisfiabile pentru o formula booleana. O atribuire de valori booleene pentru variabilele acestei expresii se numeste atribuire satisfiabila daca evaluarea expresiei dupa atribuirea valorilor da rezultat ca valoare de adevar "adevarat". Un exemplu de formula ar fi:
((x1 SAU x2) SI ((NOT x3) SI x1) SAU x4)
aceasta avand o atribuire satisfiabila x1=1 x2=0 x3=0 x4=1.
Orice formula booleana poate fi transformata in 2 forme: forma normal conjunctiva (expresia este scrisa ca o conjunctie de propozitii P1 SI P2 SI ... SI Pn, unde Pi este de forma T1 SAU T2 SAU ... SAU Tk, Tj fiind un termen care poate sau nu sa fie negat) si forma normal disjunctiva (expresia este scrisa ca o disjunctie de propozitii in interiorul carora exista doar conjunctii intre termeni).
Date de intrare
Fişierul de intrare 2sat.in ...
Date de ieşire
În fişierul de ieşire 2sat.out ...
Restricţii
- ... ≤ ... ≤ ...
Exemplu
2sat.in | 2sat.out |
---|---|
This is some text written on multiple lines. | This is another text written on multiple lines. |
Explicaţie
...