1. 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=Fdenotă 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
2. Determinarea realizabilității Urmăriți codul scris la curs și explicați ce pași se parcurg în determinarea realizabilității unei formule propoziționale.
Folosiți o formulă în CNF produsă de acest generator. Selectați în dreapta Problem Type: Random k-Sat, 3 literale pe clauză, 5 variabile, 6 clauze. În fișierul random_ksat.dimacs generat, fiecare rând încheiat de 0 reprezintă o clauză, întregii negativi reprezintă negații. Deci 3 -6 -1 0 reprezintă p3 ∨ ¬ p1 ∨ ¬ p6.
Puteți să vă ajutați în explicații adăugând tipăriri la codul scris (ex. ce atribuiri se încearcă pentru ce variabile, ce clauze se simplifică) sau doar să urmăriți codul "cu creionul pe hârtie".