Realizabilitatea formulelor boolene

Tema pentru laboratorul 7

1. Desenați diagrama de decizie binară pentru o funcție booleană aleasă astfel: să aibe cel puțin trei variabile propoziționale, și cel puțin două din acestea să apară de două ori în expresia funcției.

2. Determinați dacă o formulă propozițională în formă normală conjunctivă e realizabilă. Alegeți o formulă cu cel puțin 5 variabile propoziționale, 5 clauze, iar fiecare clauză să aibe între 2 și 4 literale.

3. Scrieți o funcție care să returneze forma normală conjunctivă pentru o formulă booleană dată. Folosiți următorul tip pentru formulă:

type bexp = V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp
Rezolvați problema în doi pași:
a) scrieți întâi o funcție care propagă negația în adâncime (cu relațiilr lui de Morgan) și returnează o formulă echivalentă, dar în care negația se aplică doar direct propozițiilor
b) apoi scrieți o funcție care folosește distributivitatea pentru a propaga disjuncția în adâncime (astfel încât sub disjuncție să nu se mai afle vreo conjuncție)

Probleme propuse

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

2. Considerăm formule propoziționale reprezentate prin tipul

type bexp = V of string
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp
care sunt în formulă normală conjunctivă, adică nu există subexpresii And într-o expresie Or, și negația se aplică doar literalelor.
Scrieți o funcție care ia ca parametru o astfel de formulă și returnează o reprezentare ca listă de liste de clauze .


Marius Minea
Last modified: Mon Nov 4 23:20:00 EET 2013