Realizabilitatea formulelor boolene

Tema

1: Or(a, b)
2: Neg c
3: And(1, 2)

Probleme propuse

2. Formula ca listă de clauze Considerăm formule propoziționale reprezentate prin tipul

type bexp = V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp

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 [] []

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. Transformarea Tseitin Scrieți o funcție care ia ca parametru o formulă și returnează transformarea Tseitin a ei. Folosiți tema, prin care obțineți numerele pentru fiecare subformulă (din care puteți crea noi propoziții, p_n), apoi transformați fiecare operator în parte.

5. Operatorul Nand Scrieți o funcție care ia ca parametru o formulă și returntează 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. 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.