Realizabilitatea formulelor boolene

Pentru problemele cu forma normală conjunctivă de mai jos folosiți reprezentația literalilor de la curs: 

    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 literale) ș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 literalelor care apar cu o singură polaritate
c) Știind că unul (sau mai multe) literale 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 * 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. Atribuiri adevărate Scrieți o funcție care ia ca parametru o formulă și a) returnează, b) tipărește 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: atribuiți o propoziție (cu F/T), simplificați formula, și continuați recursiv.

Indicații detaliate Rezolvăm întâi o problemă mai simplă: generăm toate șirurile de n biti (0 sau 1), și fie le tipărim, fie le punem într-o listă. 

let printbits =
  let rec printb lst n =
    if n > 0 then (
      printb (0::lst) (n-1);
      printb (1::lst) (n-1);
    ) else (List.iter print_int (List.rev lst); print_newline())
  in printb [] 

let allbits =
  let rec allb res lst n =
    if (n > 0) then allb (allb res (1::lst) (n-1)) (0::lst) (n-1)
    else List.rev lst :: res
  in allb [] []
Ambele funcții recursive au un parametru lst care acumulează lista cu combinația de biți deja generată. Când parametrul n, scăzând, ajunge la 0, au fost generați toți biții, și ai se tipăresc, sau se adaugă la parametrul res, o listă de liste (șiruri de biți).
Când n > 0, alegem pe rând bitul curent ca fiind 0 sau 1, îl adăugăm combinației existente (lst) și apelăm funcția recursiv. În cazul acumulării unei liste, rezultatul returnat de primul apel e dat ca parametru la al doilea apel.
Problema noastră e similară: trebuie să generăm combinații de atribuiri pentru variabilele din formulă, și să le tipărim / reținem pe cele care fac formula realizabilă.
Am prezentat deja o funcție pentru simplificarea unei formule (exercițiul 2). Rămâne să decidem asupra unei variabile pe care să o atribuim succesiv cu false și true. Putem scrie o funcție care parcurge o formulă și returnează orice variabilă (de exemplu prima întâlnită) sau, evitând repetarea parcurgerii, putem modifica funcția de simplificare pentru a returna o pereche: formula simplificată și una din variabilele rămase (sau șirul vid "").
Față de problema anterioară, lista lst nu va fi de întregi 0/1, ci de perechi string * bool: variabilă și valoare, de exemplu ("a", true). Evident, funcția mai ia ca parametru o formulă (și nu un întreg). Condiția de oprire e dată de valoarea formulei după simplificare. 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ă.

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

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 (de tipul bform) Or(And(V "a", V "b"), And(Neg(V "a"), Neg(V "c"))) poate fi reprezentată în tipul iteform ca ITE("a", P "b", N "c")
a) Scrieți o funcție care obține lista tuturor propozițiilor dintr-o formulă definită cu constructorii V/Neg/And/Or (fără constante boolene)
Atenție, două tipuri nu pot avea variante numite la fel, deci nu combinați problema cu tipul literal, etc.
b) Scrieți o funcție care ia ca parametru o formulă definită cu V/Neg/And/Or și returnează transformarea ei în arbore de decizie binar (tipul iteform), aplicând recursiv descompunerea Shannon (după o nouă variabilă) pentru fiecare din cele două subformule.
(Puteți folosi lista de variabile de la punctul a) sau preferabil direct, găsind la fiecare pas o variabilă cu funcția findvar din tema 6.). Tratând ca și cazuri de bază atât constantele boolene cât și propozițiile și negațiile lor, nu mai trebuie să faceți simplificarea de la punctul c)
c) Simplificați ultimul nivel al arborelui pentru a obține, pe cât posibil, fie o propoziție, fie negația ei (și nu constante boolene). Deci, simplificati if p then true else false în p, și if p then false else true în not p (am folosit scrierea ML; dealtfel ar trebui să faceți asta și când scrieți cod).
d) Simplificați arborele renunțând la deciziile inutile
e) Tipăriți un arbore de decizie în sintaxă if-then-else

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

6. Transformarea Tseitin a) Scrieți o funcție care parcurge o formulă și tipărește câte un număr (distinct) pentru fiecare operator întâlnit (folosiți un parametru-acumulator incrementat la fiecare operator)
b) Adaptați funcția de mai sus așa încât pentru fiecare operator să tipărească și operanzii lui: dacă sunt propoziții, numele lor, altfel numerele operatorilor care produc operanzii.
c) Adaptați funcția de la b) încât să nu dea numere negațiilor aplicate direct la propoziții (ci să le tipărească direct)
d) Scrieți o funcție care ia ca parametru o formulă și returnează transformarea Tseitin a ei. Folosiți punctul c), prin care obțineți numerele pentru fiecare operator/subformulă (din care puteți crea noi propoziții, p_n), și apoi tipăriți relația care leagă noua propoziție de operanzii care o produc.

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

8. Rezoluția
a) 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.
b) Scrieți o funcție care ia ca parametri o propoziție și două liste: cu clauze care conțin propoziția, și respectiv, propoziția negată. Returnați lista tuturor rezolvenților pentru propoziția dată.
Indicație Problema ne cere de fapt construirea unui produs cartezian sub formă de listă (construim m * n clauze noi dintr-o pereche cu m clauze și n clauze). Putem consulta exemplul din sec. 4.3. Mai trebuie să eliminăm din clauze propoziția în raport cu care se face rezoluția -- putem face asta într-un pas preliminar, cu List.filter sau chiar să rezolvăm punctul a) astfel încât să pună propoziția respectivă în capul fiecărei clauze. Pentru concatenarea a două clauze putem folosi List.rev_concat (e final-recursivă în primul argument, iar ordinea nu contează).
c) Folosind cele de mai sus, determinați dacă o formulă e realizabilă, adăugând succesiv la lista de clauze toți rezolvenții pentru un literal, și ștergând clauzele din care s-au obținut, până nu se mai pot obține rezolvenți. Formula e nerealizabilă dacă se obține clauza vidă, și nerealizabilă în caz contrar.
Indicație Scriem o funcție recursivă care primește o listă de clauze. Folosim problema 1, care ne returnează literalele care apar cu ambele polarități. Dacă nu există, ne oprim, formula e realizabilă. Altfel, alegem un astfel de literal. De la punctul a), obținem trei liste de clauze: cele cu literalul, cu negația lui, si cele care nu-l conțin. De la punctul b), obținem lista tuturor rezolvenților. Dacă vreunul din rezolvenți e clauza vidă, formula e nerealizabilă. Altfel adăugăm rezolvenții la lista clauzelor fără literalul selectat, și cu această listă reluăm apelul recursiv.

Marius Minea
Last modified: Sun Nov 15 17:20:00 EET 2015