.dsy:it. - Spiegazione DPLL

.dsy:it.
//www.dsy.it

Spiegazione DPLL

Posted by st1v on 05-06-2011 16:02

Qualche anima buona mi può spiegare come funziona la procedura di DPLL? Trasformo la formula in fnn, poi in fnc (e fin lì ok), poi prendo l'insieme delle clausole, che sarà nella forma C0={C1,C2,C3,...}, e applico le 9 regole.... ma come? Grazie mille a chiunque vorrà aiutarmi.

EDIT: rifacendo gli esercizi passo per passo ho più o meno capito i passaggi, però faccio fatica a "finire" l'esercizio, ad es. quando ho {p=1, q=1} |- {not q} come devo procedere? Non ho ben capito le regole di asserzione e del letterale puro...