type lit = P of string | N of string
Un exemplu de formulă ca listă de clauze e: [[P "a"; P "b"; N "c"]; [N "a"; P "c"]; [P "a"; N "b"]]
1. Polaritatea literalilor
a) Scrieți o funcție care ia ca parametru o formulă în formă normală conjunctivă (listă de liste de literali) și verifică dacă un literal apare doar cu aceeași polaritate (pozitiv sau negat).
b) Scrieți o funcție care returnează mulțimea tuturor literalilor care apar cu o singură polaritate
c) Știind că unul (sau mai mulți) literali au aceeași polaritate, scrieți o funcție care returnează o formulă simplificată (realizabilă dacă și numai dacă formula originală e realizabilă), înlocuind toți literalii cu o singură polaritate cu valoarea cea mai avantajoasă.
d) Rezolvați problemele de mai sus în varianta că un literal e reprezentat de un întreg nenul (pozitiv sau negativ). Deci numărul 5 va reprezenta propoziția p5, iar numărul -5 pe ¬ p5
2. Forma normală conjunctivă Considerăm formule propoziționale reprezentate prin tipul
type bexp = V of string Neg of bexp And of bexp * bexp Or of bexp * bexpa) Scrieți o funcție care verifică (returnează true) dacă o formulă e în formulă normală conjunctivă, adică nu există subexpresii And într-o expresie Or, și negația se aplică doar propozițiilor.
3. Atribuiri adevărate
Scrieți o funcție care ia ca parametru o formulă și
a) tipărește b) returnează mulțimea tuturor atribuirilor pentru care formula
e adevărată. Se acceptă atribuiri parțiale (care dau valori doar unor
propoziții, suficient ca să facă formula adevărată).
Indicație: Scriem o funcție auxiliară care simplifică succesiv formula,
reținând într-un parametru-acumulator o listă sau dicționar de atribuiri alese până în acel moment.
Condiția de oprire e dată de valoarea formulei cu atribuirile / simplificările deja făcute. Dacă obținem B true, lista atribuirilor de până
acum se poate tipări / reține în lista de soluții res. Dacă
obținem B false, formula nu e realizabilă cu atribuirile
curente, și nu facem nimic / returnăm lista de soluții nemodificată.
Altfel, formula nu e constantă, și găsim o variabilă pe care
o atribuim succesiv cu false și true, adâugând-o la
lista/dicționarul de atribuiri trimis ca parametru.
4. Sumă de produse
Scrieți o funcție care primește o formulă sub formă de arbore de decizie (vezi problema de la temă)
și tipărește formula în formă de sumă de produse (formă normală disjunctivă, disjuncție de conjuncții), urmând toate căile și tipărind acele combinații pentru care care valoarea formulei e true. Pentru exemplul de arbore de decizie binar dat la curs, funcția ar tipări ~x1*x2*x3+x1*~x2*x3+x1*x2*x3
Puteți simplifica tipărirea renunțând la '+' și tipărind în schimb fiecare conjuncție (produs) pe un rând separat.
5. Operatorul Nand Scrieți o funcție care ia ca parametru o formulă și returnează o formulă scrisă folosind doar operatorul Nand(a, b) = ¬(a ∧ b). Folosiți relațiile: 1) Neg a = Nand(a, a); 2) And(a, b) = Neg(Nand(a, b)); 3) Or(a, b) = Nand(Neg a, Neg b)), iar in 2) si 3) aplicati din nou 1).
6. Clauze cu literal pozitiv / negativ
Scrieți o funcție care la ca parametri o listă de clauze și o propoziție
și returnează o pereche de liste: clauzele care conțin propoziția, și respectiv, propoziția negată.
Indicație O soluție simplă e folosirea lui List.filter
de două ori pe lista de clauze, având ca predicat un test cu List.mem
pentru a determina dacă fiecare clauză în parte conține literalul (respectiv negația lui). Sau putem face o singură parcurgere cu List.fold_left,
returnând direct perechea de liste.