Esercizio Clicca QUI per vedere il messaggio nel forum |
marcoguillermaz |
Ciao a tutti sto facendo i temi d'esame per il compitino e mi è balzato all'occhio un problema con la dpll su un esercizio.
Mi date una mano??
allora nei due temi d'esame c'è questa espressione :
((q->p)->p)->q
l'altra è molto simile
((q->p)->q)->q
In entrambe chiede di verificare se siano tautologie, io come da procedura le nego, arrivando in fondo mi trovo una situzione di soddisfacibilità in entrambe le espressioni.
Potete verificare anche voi???
GRazie |
s4lv0 |
Ciao,
la prima:
¬[((q->p)->p)->q]
mi viene:
C={q v p, ¬p v p, ¬q}
ed è SAT
la seconda:
¬[((q->p)->q)->q]
mi da:
C={q v q, ¬p v q, ¬q}
ed è UNSAT |
marcoguillermaz |
Grazie mille per la risposta, il mio solo dubbio era come trattare i due casi in cui mi trovo :
p V p e p V not P, per il fatto che in entrambe sicuramente q = 0, visto il not q, ma in queste due come funziona ....??? |
s4lv0 |
Figurati,
quando poni q=0, devi cancellare tt le clausole in cui compare ¬q, mentre cancelli solo il letterale da qll in cui compare q e viceversa se poni q=1 |
marcoguillermaz |
Questo è chiarissimo, ma se noti quando ho la prima espressione in fnc, mi trovo p V p in questo caso ho capito, ma se mi trovo :
p V p, not q V p , not p
come mi devo comportare ??? |
s4lv0 |
ti viene così:
p=0 |-{clausola vuota, ¬q}
quindi UNSAT |
marcoguillermaz |
Ti ringrazio, se mi dici solo come funziona quando devo per forza porre p = 0 e mi ritrovo p V p ? lo devo considerare come clausola vuota?? |
s4lv0 |
certo, visto che ogni clausola la puoi considerare in "or" con la clausola vuota
quindi nel tuo esempio: p v p v clausola vuota ....xciò quando cancelli i due letterali ti rimane la clausola vuota |
franky_fs |
Eventualmente per poter verificare se hai sbagliato o meno potresti applicare i valori SAT trovati con la DPLL alla formula di partenza, se il suo valore è FALSE, allora l'esercizio è corretto: hai trovato dei valori che dimostrano che la formula non è una tautologia. Se esce TRUE c'è qualcosa che non va. |
|
|
|