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=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 * iteformITE(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.
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".