Logică propozițională. Realizabilitatea formulelor boolene

Dacă nu e specificat altfel, pentru problemele cu forma normală conjunctivă de mai jos folosiți următoarea reprezentare a literalilor:
type lit = P of string | N of string
Ca exemplu, formula (a ∨ b ∨ ¬ c) ∧ (¬ a ∨ c) ∧ (a ∨ ¬ b) poate fi scrisă ca listă de clauze: [[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 p₅, iar numărul -5 pe ¬ p₅

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 * bexp

a) 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.
b) Presupunând că formula e în formă normală conjunctivă, scrieți o funcție care ia ca parametru o astfel de formulă și returnează o reprezentare ca listă de clauze .

3. 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.

4. 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.

5. Arbori de decizie. Orice formulă booleană f poate fi descompusă în raport cu o propoziție p după formula f = p ∧ f|_p=T ∨ ¬p ∧ f|_p=F (numită descompunere Shannon sau Boole), unde f|_p=T și respectiv f|_p=F denotă formulele obținute din f substituind pe p cu valorile true, respectiv false. Altfel scris, f = if p then f|_p=T else f|_p=F. Această descompunere e folosită și în arborii / diagramele de decizie binare discutate la curs. Folosiți tipurile

type bform = B of bool | V of string | Neg of bform
             | And of bform * bform | Or of bform * bform
type iteform = C of bool | P of string | N of string | ITE of string * iteform * iteform

ITE(p, f1, f0) înseamnă if p then f1 else f0. De exemplu, formula Or(And(V "a", V "b"), And(Neg(V "a"), Neg(V "c"))) poate fi reprezentată ca ITE("a", P "b", N "c"), de tipul iteform.
Varianta C of bool are tot înțelesul de constantă booleană, dar nu putem folosi aceeași etichetă (B) în două tipuri. P reprezintă o variabilă pozitivă și N negația unei variabile.
a) Scrieți o funcție care ia ca parametru o formulă de tipul bform și returnează transformarea ei în arbore de decizie binar (tipul iteform), aplicând recursiv descompunerea Shannon pentru fiecare din cele două subformule.
(Dacă formula nu e constantă, găsiți la fiecare pas o variabilă cu funcția find_var de la cursul 6).
b) Scrieți o funcție care tipărește un arbore de decizie în sintaxa if-then-else din ML
c) (opțional) Simplificați ultimul nivel al arborelui, transformând ITE("a", C true, C false) în P "a" și similar pentru negație. (Dealtfel, ar trebui să faceți asta și în cod, if x then true else false e echivalent cu x.
d) (opțional) Simplificați arborele renunțând la deciziile inutile

6. 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).

7. Sumă de produse Scrieți o funcție care primește o formulă sub formă de arbore de decizie (vezi problema de mai sus) ș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.

Marius Minea

Last modified: Tue Nov 7 9:00:00 EET 2017