Riavvia casuali per istanze insoddisfacenti

Question

Nel peggiore dei casi, la soddisfazione booleana (supponendo che P! = NP) richiede tempo esponenziale. Tuttavia, i moderni risolutori SAT che utilizzano varianti di DPLL sono in grado di risolvere istanze sufficienti per essere utili nella pratica.

Una tecnica utilizzata, che ha mostrato buoni risultati nella pratica, è il riavvio casuale. Intuitivamente, riavviamento casualmente significa che c'è la possibilità di diventare più fortunati nell'incontrare i compiti variabili giusti che porterebbero a una soluzione rapida.

La stessa intuizione suggerisce che ciò dovrebbe essere molto più efficace quando l'istanza del problema è in realtà soddisfacente (quindi devi solo indovinare una serie di incarichi variabili che costituiscono una soluzione) che se non lo è (quindi in linea di principio devi controllare tutto possibile Assegnazioni comunque, sezioni di modulo dello spazio di ricerca che possono essere saltate tramite tecniche come la propagazione unitaria e il backtracking non cronologico, che almeno non sono ovviamente sensibili alle ipotesi iniziali).

La seconda intuizione è corretta? I riavvii casuali sono in effetti molto più efficaci, in media, nei casi in cui l'istanza del problema è in realtà soddisfacente?