(LOGICA)Soddisfacibilità formula in CNF

[Pask891]

Sia $ f in CNF $ il seguente insieme di clausole:

$ {{-p0,p1,-p2,-p3},{-p1,p2,-p4},{p1,p2,-p3,p4},{p1,-p2,p3},{p0},{p3},{-p1,p2,p3,p1}} $

-p indica NOT;
Bisogna stabilise se f è soddisfacibile;

Scelgo p3 procedo in questo modo:
se p3 compare nelle clausole, cancello le clausole, se p3 compare con segno opposto cancello p3;

p3(f)= $ {{-p0,p1,-p2},{-p1,p2,-p4},{p1,p2,p4},{p0}} $=g

Faccio la stessa cosa con un altro letterale:

p0(g)= $ {{p1,-p2},{-p1,p2,-p4},{p1,p2,p4}} $

Il punto è che non sono sicuro che si procede in questo modo; il procedimento si basa sulle regole di Davis-Putnam.
Ed inoltre non so come capire se è soddisfacibile;
Potreste darmi dei chiarimenti?
Grazie.

[enzo221]

E' lo stesso esercizio che nn riesco a fare nemmeno io,spero che qualcuno posti x capire come risolverlo

[enzo221]

Ciao,allora per risolvere questo esercizio di logica devi applicare i seguenti teoremi:Teorema di Decomposizione,Clausola Unitaria e Basica Pura,vedi se riesci a capire questi tre teoremi,l'esercizio è abbastanza banale.Se non ci riesci posta di nuovo che ti spiego

Ciao!