PDA

Visualizza versione completa : Complessità SAT di CNF e DNF



Vegeta1485
02-05-2009, 22.52.16
Non so se questa sia la sezione giusta per parlarne ma visto che non mi sembra ci sia una sessione "pippe mentali sulle complessità algoritmiche" scrivo qui dove magari può essere letto da qualcuno che mi saprà rispondere ^^", in ogni caso se dovesse esistere una sezione più consona per questa domanda trasferite pure ^^.

Allora ho un problema a capire come si calcolano le complessità di algoritmi che determinino la soddisfacibilità delle CNF e di algoritmi che determinino quella delle DNF.

Se non sbaglio la complessità di SAT per le CNF dovrebbe essere NP-Completa mentre quella delle DNF dovrebbe essere polinomiale.

Ora io pensavo che per calcolare la complessità di SAT si prendesse in considerazione come input le occorrenze delle variabili in ingresso, ovvero per una CNF o una DNF con: 10 p, 20 q, 30 r, 20 not-p, 30 not-q e 10 not-r si prendesse in considerazione come n per calcolare la complessità 120, ma se non ho capito male quello che mi è stato detto che invece viene preso in considerazione 3.

Ora il mio dubbio è ma se funziona così, come posso trovare la soddisfacibilità di una DNF al più in tempo polinomiale? basti pensare a una DNF strutturata nel seguente modo:

(X1 \/ not-X1 \/ (tutte le 2^n-1 combinazioni possibili delle altre variabili e delle loro negazione)) /\ (X2 \/ not-X2 \/ (tutte le 2^n-1 combinazioni possibili delle altre variabili e delle loro negazione)).

E già si hanno 2^n clausule che richiedono almeno 2*2^n ovvero 2^n+1 passi di computazione per essere lette, e questo non è neanche il caso peggiore poiché 1) si può ripetere per tutte le Xi 2) si stanno prendendo in considerazione solamente clausule di lunghezza fissa n+1.

Ho già cercato su google qualcosa che mi aiutasse a capire come clacolare la complessità di SAT o un algoritmo che risolva le DNF in tempo polinomiale, ma non ho trovato niente (almeno in italiano con l'inglese non me la cavo molto bene).

Ho provato anche a cercare di capire come convertire il problema della fattorizzazione in numeri primi in SAT per vedere se la soluzione a SAT che ho in testa potasse a delle migliorie almeno in questo caso, ma l'unica cosa che ho trovato sono delle slide in inglese un po' troppo sintetiche.

DIAZE
03-05-2009, 07.38.15
Sezione giusta :look: